|
|
Pohyb v projektu ENTI
Bajer, Lukáš ; Šerý, Ondřej (oponent) ; Brom, Cyril (vedoucí práce)
Projekt ENTI je simulátor prostředí, které je podobné lidskému světu. Žijí v něm autonomní agenti nazývaní enti, kteří se o svět starají. K naplňování svých úkolů a životních potřeb potřebují často hledat po svém světě cestu. Tato práce je zaměřena na skripty, které toto hledání a následné procházení cest řídí. Pohyb entů mezi místnostmi vylepšuje hierarchickou verzí algoritmu A*, čímž snižuje nároky na procesor při hledání delších cest. Dále pak rozšiřuje skripty pro pohyb po místnosti, sledování a vyhýbání se cizím entům a hledání předmětů.
|
|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Diplomová práce předkládá nástroj pro analýzu modelů ve specifikačním jazyce DeSpec a pro jejich překlad do modelovacího jazyka Zing. Výsledné modely pak mohou být verifikovány model checkerem Zing. Jazyk DeSpec je navržen především pro specifikaci prostředí, ve kterém pracují ovladače operačních systémů rodiny Windows NT. Umožňuje abstrahovat toto prostředí objektově orientovaným způsobem a používá formule lineární temporální logiky k popisu pravidel, jejichž splnění jádro OS Windows od ovladačů vyžaduje. Jazyk Zing je navržen pro popis vykonavatelných modelů software včetně paralelismu, které mohou být dale zkoumány model checkerem Zing. Vlastnosti k ověření jsou vyjádřeny příkazy assert. Dosud neexistoval způsob, jak automaticky extrahovat ze specifikace v DeSpecu model, který by mohl být formálně verifikován model checkerem. Překladač z DeSpecu do Zingu hraje v tomto úkolu zásadní roli. Práce ukazuje, že je možné překládat specifikace v DeSpecu do modelů v Zingu a tedy že DeSpec je vhodným jazykem pro model checking cílového prostředí. Uvedený nástroj umožňuje kontrolu správnosti specifikace v DeSpecu a za omezení daných absencí dalších nezbytných nástrojů umožňuje překlad vybrané podmnožiny specifikací do Zingu.
|
|
|
Memory Representation for Model Checker of C/C++
Kouba, Jan ; Kofroň, Jan (oponent) ; Šerý, Ondřej (vedoucí práce)
V předložené práci je popsán návrh a C++ implementace nově vytvořeného paměťového modulu, který bude použit k reprezentaci paměti zkoumaného programu v GIMPLE Model Checkeru (explicit state model checkeru). Modul se liší od většiny ostatních code model checkerů v tom, že umožňuje uložit do simulované paměti libovolné C++ objekty splňující jisté rozhraní. To umožňuje ukládat například data hodnot spolu s jejich typy, symbolické hodnoty používané při symbolickém vykonávání programu nebo predikáty o hodnotách používané při predikátové abstrakci. Pro efektivní ukládání stavů, kanonikalizaci haldy a výpočet hashe stavu používá modul delta ukládání, inkrementální hashování a inkrementální kanonikalizaci haldy.
|
|
|
Unit checking for Java IDE
Kebrt, Michal ; Parízek, Pavel (oponent) ; Šerý, Ondřej (vedoucí práce)
Code model checking is a rapidly advancing research topic. However, apart from very constrained scenarios (e.g., veri cation of device drivers by SLAM), the code model checking tools are not widely used in general software development process. We believe that this could be changed if the developers could use the tools in the same way they already use testing tools. In this work, we present the UnitCheck tool, which enhances the standard unit testing of Java code with model checking. A developer familiar with unit testing can apply the tool on standard unit test scenarios and bene t from the exhaustive traversal performed by a code model checker, which is employed inside UnitCheck. Two well-known Java tools are integrated in UnitCheck. JUnit is used as a testing framework and Java PathFinder provides the model checking capability. The UnitCheck plugin for Eclipse presents the checking results in a convenient way known from unit testing, while providing also a verbose output for the expert users. The UnitCheck Ant task allows to incorporate unit checking in the standard Java development and build process.
|
|
|
Interpretr stavových automatů popsaných jazykem SCXML
Baláž, Ján ; Bulej, Lubomír (oponent) ; Šerý, Ondřej (vedoucí práce)
V súčasnosti vzniká potreba pristupovať ku rôznym programátorským úlohám alternatívnymi postupmi. Jedným z takýchto postupov je zápis pomocou stavových automatov. Ako riešenie sa ukazuje novo vznikajúci štandard W3 Consorcia, nazvaný SCXML. V súčasnosti už existuje niekolko rôznych implementácii, ktoré však kvôli svojej rozsiahlosti nemusia byť vhodné pre jednotlivcov, alebo malé a stredné rmy. Tieto spoločnosti potrebujú nástroje, ktoré si môžu jednoducho prispôsobovať na svoje vlastné projekty. Cielom práce je vytvoriť interpreter stavových automatov popísaných jazykom SCXML, ktorý bude splňať popísané podmienky. Snahou je implementovať maximálnu časť špecikácie SCXML. Práca bude vytvorená v jazyku Perl a bude podporovať operačné systémy Windows a Linux.
|
|
|
Grafický editor 3D scén pro projekt AGE
Herceg, Tomáš ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Název práce: Grafický editor 3D scén pro projekt AGE Autor: Tomáš Herceg Katedra (ústav): Katedra distribuovaných a spolehlivých systémů Vedoucí bakalářské práce: Mgr. Pavel Ježek, Katedra distribuovaných a spolehlivých systémů E-mail vedoucího: pavel.jezek@dsrg.mff.cuni.cz Abstrakt: Cílem práce je vytvořit grafický editor, který umožní tvorbu a editaci grafických scén ve 3D prostoru. Editor by měl být realizován jako rozšiřující modul do projektu AGE. Jelikož je projekt AGE teprve ve fázi vývoje, měla by jako součást této bakalářské práce vzniknout i jeho první verze. Samotný editor vytvořený v rámci práce by měl podporovat vytváření základních primitivních objektů, manipulaci s jednotlivými vrcholy, stěnami a částmi těchto objektů, a dále pak implementovat základní nástroje pro mapování textur. Jako cílová platforma bude použito prostředí .NET Framework a pro zobrazování grafických výstupů je doporučeno použít technologie Windows Presentation Foundation a DirectX. Klíčová slova: Počítačová grafika, Windows Presentation Foundation, DirectX, 3D
|
|
|
Ekonomická tahová strategická hra
Hermann, Lukáš ; Šerý, Ondřej (oponent) ; Lánský, Jan (vedoucí práce)
V předložené práci se zabýváme návrhem a implementací ekonomické tahové strategie. Po popsání a analýze základních pravidel hry vytváříme objektový model, skládající se ze základního rozhraní, konkrétních tříd a jejich propojení mezi sebou. Dále podrobně rozebíráme ekonomické modely a další související algoritmy použité v jejich metodách včetně jejich zapsání v pseudokódu. Nakonec tvoříme editory vlastností a chování herních objekt a zabýváme se tvorbou originálního gra fického interface s konkrétními vizuálními komponentami, z nichž sestavujeme uživatelské prostředí.
|
|
|
Sewing pattern editor
Černý, Martin ; Poch, Tomáš (oponent) ; Šerý, Ondřej (vedoucí práce)
Konstrukce střihů je základní součástí oděvního návrhářství. Předmětem této práce je implementace editoru textilních střihů, který by vyhovoval potřebám nezávislých oděvních návrhářů a výrobců zakázkového šatstva. Práce v editoru je velmi blízká ručnímu navrhování střihu a program je tedy pro návrháře snadno použitelný. Implementace pokrývá nejdůležitější oblasti navrhování střihů. Střihy v programu vytvořené mohou být použity pro různé zákazníky, protože se automaticky přizpůsobují zadaným tělesným mírám.
|
|
|
Frontend pro matematicky vyhledavac
Klíma, Jaroslav ; Mišutka, Jozef (vedoucí práce) ; Šerý, Ondřej (oponent)
Elektronický zápis matematických výrazů získává na důležitosti se stoupající tendencí využití softwaru v každodenním živote. Školy začnají podporovat e-learning, studenti i vědci prezentují své práce na internetu a vyhledávače se dokáží vypořádat se stále komplexnějšími dotazy. V předložené práci shrnu stav dostupných aplikací které podporují vkládání matematických výrazů a které by bylo možno využít jako uživatelské rozhraní pro matematický vyhledávač EgoMath. Protože žádná z nich nesplňuje naše požadavky, prezentuji zde návrh a implementaci nového matematického uživatelského rozhraní zaměřeného na zjištené nedostatky existujících řešení. Cílem nového rozhraní je umožnit uživateli zadání matematického výrazu ve formátu který dokáže zpracovat cílová aplikace. Výraz obsahující symboly z velké množiny je nutno zadávat pomocí omezeného počtu kláves. Toto musí být intuitivní a aplikace by měla uživateli aktivně pomáhat grafickou nápovědou založenou na rozpoznávání vkládaného výrazu v reálném čase.
|
|
|
Vizualiazace algoritmů pomocí uživatelských scriptů
Šebesta, Jiří ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Cílem této práce bylo vytvoření programu AlgoShow sloužícího pro názornou ukázku fungování algoritmů. Algoritmy se zapisují jako skripty, ve kterých je možno využívat různých funkcí pro grafické znázornění běhu algoritmu. Práce se zabývá programem AlgoShow jak z uživatelského, tak i z programátorského hlediska. Součástí je krátký úvod do problematiky vizualizace algoritmů, srovnání programu AlgoShow s podobnými existujícími nástroji, popis návrhu a implementace programu včetně způsobu interpretace skriptu. Dále práce obsahuje charakteristiku základních funkcí programu a zejména podrobný popis skriptovacího jazyka.
|
host ::
RSS.