|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Jančík, Pavel (oponent)
Název práce: Prezentace výsledků kontroly softwarového modelu skrz ladící rozhraní Autor: Tomáš Kohan Katedra: Katedra softwarového inženýrství Vedoucí diplomové práce: RNDr. Ondřej Šerý, Ph.D., Katedra distribuovaných a spolehlivých systémů Abstrakt: Cílem této práce je navrhnout a implementovat nové ladící rozhraní programu Java PathFinder. Vhodným prostředím pro toto rozhraní byl zv- olen vývojový nástroj Eclipse. Vytvořené rozhraní graficky vizualizuje výstupy programu JPF a jednotlivé detaily stavu pozastaveného virtuálního stroje (JVM), zvláště pak seznam proměnných a jejich hodnot. Za tímto účelem jsou vytvořeny dva podprojekty, a to debug4jpg a JPFDeb.core. Projekt debug4jpf kontroluje a komunikuje s instancí JPF. JPFDeb.core pak ve formě zásuvného modulu pro Eclipse poskytuje takové uživatelské rozhraní, které je podobné standardnímu rozhraní ladícího programu pro Javu. Oba projekty mezi sebou komunikují přes ad hoc komunikační protokol, který byl navržen pro tento účel. Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Jančík, Pavel (oponent)
Název práce: Prezentace výsledků kontroly softwarového modelu skrz ladící rozhraní Autor: Tomáš Kohan Katedra: Katedra softwarového inženýrství Vedoucí diplomové práce: RNDr. Ondřej Šerý, Ph.D., Katedra distribuovaných a spolehlivých systémů Abstrakt: Cílem této práce je navrhnout a implementovat nové ladící rozhraní programu Java PathFinder. Vhodným prostředím pro toto rozhraní byl zv- olen vývojový nástroj Eclipse. Vytvořené rozhraní graficky vizualizuje výstupy programu JPF a jednotlivé detaily stavu pozastaveného virtuálního stroje (JVM), zvláště pak seznam proměnných a jejich hodnot. Za tímto účelem jsou vytvořeny dva podprojekty, a to debug4jpg a JPFDeb.core. Projekt de- bug4jpf kontroluje a komunikuje s instancí JPF. JPFDeb.core pak ve formě zásuvného modulu pro Eclipse poskytuje takové uživatelské rozhraní, které je podobné standardnímu rozhraní ladícího programu pro Javu. Oba projekty mezi sebou komunikují přes ad-hoc komunikační protokol, který byl navržen pro tento účel. Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
|
|
|
Redakční systém s podporou dynamicky generovaného obsahu
Nádraský, Václav ; Ježek, Pavel (vedoucí práce) ; Šerý, Ondřej (oponent)
Předmětem práce je návrh a vytvoření redakčního systému, který je snadno rozšiřitelný a umožňuje vytvářet webové aplikace z předem připravených komponent, které je možné libovolně umisťovat do obsahu stránek. Tyto komponenty mohou obsahovat i složitou aplikační logiku, která je ale nezávislá na rozložení ovládacích prvků na stránce. Redakční systém dovoluje tvořit obsah obsahující libovolné informace z databáze bez nutnosti programovat nebo psát SQL dotazy.
|
|
|
Vektorový grafický editor pro projekt AGE
Šebetovský, Jan ; Ježek, Pavel (vedoucí práce) ; Šerý, Ondřej (oponent)
Předložená práce se zabývá tématem vytvoření vektorového gra ckého editoru, který by bylo později možné zakomponovat do projektu AGE, jehož cílem je vytvořit integrovaný gra cký nástroj. Součástí této práce je také vytvořený základ pro tento editor, jehož předností oproti ostatním editorům je zejména práce s výrazy, pomocí kterých mohou být navázány parametry objektů na jiné objekty. Dále editor podporuje vrstvy (ve formě skupin objektů), export obrázku do bitmapových formátů a práci s Bézierovými křivkami. Navíc je program téměř zcela připraven na přidání filtrů, které vznikají jako jiná bakalářská práce.
|
|
|
Investment Strategies Simulator
Helešic, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Poch, Tomáš (oponent)
Název práce: Simulátor obchodních strategií Autor: Tomáš Helešic Katedra (ústav): Katedra softwarového inženýrství Vedoucí bakalářské práce: RNDr. Ondřej Šerý e-mail vedoucího: ondrej.sery@d3s.mff.cuni.cz Abstrakt: 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řily plnohodnotné prostředí pro psaní, vyhodnocení a zobrazení uživatelských strategií. Klíčová slova: Obchodní strategie; Technická analýza; Skriptování;
|
|
|
Software pro rozvrhování operací a evidence nástrojů pro nemocniční zařízení
Tupec, Pavel ; Šerý, Ondřej (vedoucí práce) ; Kruliš, Martin (oponent)
V současné době je ve většině nemocničních zařízeních vytvářen denní rozvrh pro operační sály ručně, nebo jen s minimálním využitím softwarových nástrojů. Důsledkem toho je občasná neefektivita rozvrhů a hlavně značná každodenní časová náročnost pro vedoucího lékaře, který by mohl využít ušetřený čas na důležitější věci ve svém oboru. Dalším důvodem vzniku této aplikace je, že data o pacientech, operacích, operačních sálech, diagnózách jsou uložena decentralizovaně v různých systémech, což značně stěžuje práci s nimi. Předmětem této práce je implementace aplikace pro tvorbu rozvrhů na operačních sálech v nemocničních zařízeních se zajištěním potřebných nástrojů a kapacit, a evidence nástrojů. Kde budou data pro o všech potřebných entitách ke generování rozvrhu uložena a spravována centrálně. Výsledný program má za úkol, zefektivnit a částečně automatizovat proces plánovaní operací.
|
|
|
Model Checking and Reduction of Behavior Protocols
Šerý, Ondřej
Behavior protokol je formalismus pro specifikaci chování softwarových komponent. V syntaxi podobné regulárním výrazům jsou definovány přípustné sekvence volání metod, přičemž se abstrahuje od vnitřních dat komponent. Jde sice o rozumnou úroveň abstrakce pro ověření bezchybnosti komunikace softwarových komponent, nicméně pro člověka muže být jeho přečtení a pochopení obtížné. Tato práce se snaží pomoci softwarovému návrháři pochopit specifikaci chování komponent. Předkládá způsob automatického ověřování platnosti obecných časových vlastností vyjádřených v lineární temporální logice spolu s dvěmi technikami redukce behavior protokolu. Redukce vzhledem ke kompozici odstraní ty části protokolu, které nejsou použity v dané kompozici komponent, a zdůrazní tak skutečné role všech komponent. Redukce vzhledem k vlastnosti vypustí ty části protokolu, které nejsou podstatné pro danou vlastnost. Takto redukovaný protokol by měl zdůraznit části, které zapříčiňují platnost dané vlastnosti.
|
|
|
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í.
|
host ::
RSS.