|
|
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.
|
|
|
GIMPLE Model Checker
Krč-Jediný, Ondrej ; Šerý, Ondřej (vedoucí práce) ; Hauzar, David (oponent)
Název práce: GIMPLE Model Checker Autor: Ondrej Krč-Jediný Katedra (ústav): Katedra distribuovaných a spolehlivých systémů Vedoucí diplomové práce: RNDr. Ondřej Šerý Ph.D. e-mail vedoucího: Ondrej.Sery@mff.cuni.cz Abstrakt: Cieľom práce je implementácia základných prvkov explicit-state model checkeru pre jazyk C - pokročilého nástroja na hľadanie chýb v programoch. Tento nástroj prehľadáva všetky možné cesty, ktorými môže byť program vykonávaný a zároveň vyskúša všetky možné kombinácie prekladania vlákien. Nástroj je založený na GIMPLE - výstupe front-endu kompilátora GCC, ktorý berie za svoj vstupný jazyk. Práca využíva predchádzajúcu prácu 'Memory representa- tion for GIMPLE Model Checker', ktorá implementuje prácu s pamäťou pre tento nástroj. Tým, že je nástroj vychádza z GIMPLE, umožňuje overovanie systémov priamo v jazyku C, naviac je ľahko rozšíriteľný na iné jazyky podporované GCC. 1
|
|
|
Skupinový diář
Florián, Jiří ; Žemlička, Michal (vedoucí práce) ; Šerý, Ondřej (oponent)
Ať si to chceme či nechceme připustit, celý náš život se skládá z plnění rozličných úkolů a událostí. A právě vytvoření návrhu aplikace pro snadné plánování úkolů a událostí je cílem této bakalářské práce. Konkrétně půjde o aplikaci, která bude vhodná pro spojení osobního i pracovního plánování, aniž by přitom došlo k jakémukoli narušení soukromí.
|
|
|
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í.
|
|
|
Peer To Peer Component Framework
Klačko, Tomáš ; Šerý, Ondřej (oponent) ; Tůma, Petr (vedoucí práce)
Peer To Peer Komponentový Framework je software, ktorý umožňuje vytvárať inštancie komponent na uzloch v sieti, ktoré splňujú požadované podmienky v dobe inštanciácie. Diplomová práca prezentuje návrh tohto software spolu s jeho prvotnou implementáciou. Framework považuje za komponentu každý vykonatelný kód. Preto vytvorenie inštancie komponenty na uzle v sieti znamená vzdialené vykonanie kódu na tomto uzle. Vzdialené vykonávanie kódu všeobecne tvorí bezpečnostný problém. Pretože framework má praktické zameranie, tak v tomto smere umožňuje využiť existujúci bezpečnostný software. Požiadavky na návrh frameworku spolu s jeho prvotnou implementáciou sú odvodené predovšetkým od jeho prípadov použitia. Dva modelové prípady sú taktiež uvedené v diplomovej práci.
|
|
|
Object-oriented Command Shell
Molnár, Martin ; Šerý, Ondřej (oponent) ; Ježek, Pavel (vedoucí práce)
Predložená práca sa zaoberá vnášaním objektovo orientovaného prístupu do programovania v príkazovom riadku. Študuje možnosti z adenia konceptov OOP a dávkového spracovania ľ a navrhuje vhodný kompromis medzi týmito prístupmi. Hlavným cieľom tejto práce je implementácia zvoleného riešenia v rodinách operačných systémov Unix a Microsoft Windows. Práca teda popisuje rozhodnutia súvisiace s implementáciou, ako aj používanie výslednej aplikácie.
|
|
|
Informační systém pro společnost na výrobu součástek do dopravní techniky
Čech, Martin ; Šerý, Ondřej (oponent) ; Kofroň, Jan (vedoucí práce)
V předložené práci studujeme návrh a konkrétní implementaci informačního systému pro malé a střední firmy. Jejím cílem je správa dat o zaměstnancích, partnerských společnostech (jak dodavatelích, tak zákaznících), jednotlivých zakázkách a samotných výrobcích. Jedná se tedy o prakticky zaměřenou aplikaci, která se skládá ze tří částí: databázové vrstvy, aplikačního serveru a klientského programu pro správu dat. Je navíc specializována na správu výrobků, jejich rozklad na elementární součástky a vytváření jejich výrobních postupů. Další významnou částí je evidence produkce zaměstnanců, díky které je možné sledovat postup vývoje zakázky a také generovat mzdu. V práci se zaměříme zejména na řešení jednotlivých částí aplikace a komunikace mezi nimi.
|
|
|
Řízení příběhu pomocí Petriho sítí - drama manager
Abonyi, Adam ; Šerý, Ondřej (oponent) ; Brom, Cyril (vedoucí práce)
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.
|
|
| |
|
|
Renonc - licitovaný mariáš
Kozmík, Václav ; Šerý, Ondřej (oponent) ; Kronus, David (vedoucí práce)
Předložená práce se zabývá vývojem aplikace pro hru licitovaného mariáše na počítači. Výsledná aplikace pro operační systém Windows umožňuje hru proti počítačovým protivníkům nebo hru po síti s lidskými protihráči. Umělá inteligence dosahuje úrovně pokročilejšího hráče mariáše, dodržuje zažité herní zvyklosti a pro řešení herních situací na konci hry používá algoritmus minimaxu. Síťová komunikace probíhá přes vlastní protokol založený na XML, což umožňuje alternativní implementaci klientské části v libovolném programovacím jazyce. Přínosem oproti stávajícím aplikacím je moderní grafi cké rozhraní, široké možnosti nastavení pravidel hry a také možnost ukládání lokálních i síťových her v jakémkoliv stavu hry. Práce popisuje možnosti aplikace z uživatelské a programátorské stránky a zahrnuje i porovnání s existujícími programy.
|
host ::
RSS.