|
|
Grafický editor 3D scén pro projekt AGE
Herceg, Tomáš ; Ježek, Pavel (vedoucí práce) ; Šerý, Ondřej (oponent)
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
|
|
|
Řízení příběhu pomocí Petriho sítí - drama manager
Abonyi, Adam ; Brom, Cyril (vedoucí práce) ; Šerý, Ondřej (oponent)
Výsledky virtuálního storytellingu se využívají v interaktivních počítačových hrách nebo v e-learningu. Osnovy virtuálních příběhů lze vnímat jako distribuovaný systém, jenž byl formalizován Carlem Adamem Petrim v jeho práci nazvané Petriho sítě. Tyto sítě již byly využity na poli virtuálního storytellingu, ale nikoliv k popisu příběhu ve virtuálním světě. V naší práci rozšiřujeme základní model Petriho sítí tak, aby byl jednoduše použitelný pro specifikaci osnov příběhu a pro jeho odehrávání a implementujeme tento model spolu s ladícími nástroji. Dále umožňujeme zápis příběhů pomocí formátu založeného na XML, který umožňuje snadnou spolupráci programátora a návrháře přiběhu.
|
|
|
Automated verification of software
Šerý, Ondřej ; Plášil, František (vedoucí práce) ; Janeček, Jan (oponent) ; Ghezzi, Carlo (oponent)
Přes výzkumné usilí věnované automatické veri kaci software, její pronikání do softwarového průmyslu je stále spíše pomalé. Toto váhání mělo několik důvodů 1) složitost posouzení jednotlivých nástrojů, 2) složitost použití nástrojů a jejich integrace do vvývojového procesu. Pro usnadnění výběru jednotlivých nástrojů je součástí práce přehled technik založených na model checkingu kódu s porovnáním technik na základě jednotných kritérií. Navíc práce obsahuje průmyslovou případovou studii používající model checker BLAST. K posouzení vhodnosti nástrojů je potřeba i odpovovídajícího vzdělání, přikládáme tedy i své zkušenosti s přípravou dvou magisterských přednášek o formálních metodách. Integrací snadno použitelného speci kačního jazyka do model checkeru BLAST, přispíváme k usnadnění použití tohoto nástroje. Mimo to představujeme koncept unit checkingu, tedy kombinace unit testingu a model checkingu kódu. Unit checking pomáhá s integrací model checkingu kódu do vývojového procesu.
|
|
| |
|
|
Unit checking for Java IDE
Kebrt, Michal ; Šerý, Ondřej (vedoucí práce) ; Parízek, Pavel (oponent)
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.
|
|
|
Memory Representation for Model Checker of C/C++
Kouba, Jan ; Šerý, Ondřej (vedoucí práce) ; Kofroň, Jan (oponent)
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.
|
|
|
State Space Symmetry Reduction for TBP Analysis
Černý, Ondřej ; Šerý, Ondřej (vedoucí práce) ; Poch, Tomáš (oponent)
Threaded Behavior Protocols (TBP) je specifikační jazyk pro modelování chování softwarových komponent. Tato práce se zaměřuje na analýzu TBP specifikací v rámci prostředí, která obsahují neomezené množšví replikovaných vláken. Takové specifikace spolu s modely možných prostředí způsobí nekonečnost stavového prostoru analýzy, který obsahuje velké množství symetrií, způsobených replikací vláken. V práci je navžena technika analýzy takových modelů, která redukuje symetrie s použitím abstrakce zvané Symbolic Counter Abstraction. Pro její použití je však nutné převést vlastnosti modelu na problém dosažitelnosti stavů vláken. Navrhovaná technika je bezpečná ve smyslu odhalení všech chyb v modelu. Na druhou stranu může způsobovat tzv. spurious erros, tj. chyby které neodpovídají skutečným chybám v modelu. Tyto chyby jsou v práci dobře identifikovány a dále jsou nastíněny způsoby jejich redukce. Práce navíc může představovat malý krok směrem k podpoře dynamického vytváření vláken v TBP specifikacích.
|
|
|
Simulátor obchodních strategií
Helešic, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Poch, Tomáš (oponent)
Předmětem této práce je vytvoření simulátoru obchodních strategií. Výsledný program umožňuje uživatelům stahovat aktuální i historická burzovní data, vizualizovat je pomocí grafů a implementovat na ně prostředky technické analýzy. Tyto komponenty jsou navrženy a propojeny tak, aby vytvořili plnohodnotné prostředí pro psaní, vyhodnocení a zobrazení uživatelských strategií.
|
|
|
Pohyb v projektu ENTI
Bajer, Lukáš ; Brom, Cyril (vedoucí práce) ; Šerý, Ondřej (oponent)
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 ; Ježek, Pavel (vedoucí práce) ; Šerý, Ondřej (oponent)
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.
|
host ::
RSS.