|
|
Verification of Textual Use-Cases
Vinárek, Jiří ; Šimko, Viliam (vedoucí práce) ; Hauzar, David (oponent)
Cílem práce je poskytnout nástroj pro formální verifikaci systému, který je popsán pomocí textových případů užití (textual use cases). Nástroj umožňuje automatické ověření invariantů vyjádřených pomocí formulí temporální logiky (CTL nebo LTL). Textová specifikace je transformována na formální model, který je pomocí NuSMV symbolického model-checkeru verifikován a případné chyby jsou zobrazeny uživateli. Výstupem je přehledný HTML report, který pomocí zpětné vazby umožňuje uživateli iterativní vývoj validních textových use-case specifikací. Architektura nástroje je volena s ohledem na znovupoužitelnost jednotlivých modulů a budoucí možné rozšíření. Powered by TCPDF (www.tcpdf.org)
|
|
|
Qt HDD benchmark
Matěna, Vladimír ; Marek, Lukáš (vedoucí práce) ; Šimko, Viliam (oponent)
Tato práce se zabývá měřením výkonnosti zařízení pro ukládání dat. Její účel je poskytnout program pro měření výkonnosti takových zařízení s grafickým rozhraním v prostředí Linuxu. Grafické rozhraní se snadno používá a zobrazuje výsledky měření v reálném čase. Navíc bylo několik běžných zařízení otestováno tímto programem. Zajímavé výsledky byly krátce popsány stejně jako faktory, které je ovlivnily. Obecné faktory ovlivňující výsledky v prostředí Linuxu byly také popsány.
|
|
|
IDE-supported development of component-based applications
Hermann, Lukáš ; Bureš, Tomáš (vedoucí práce) ; Šimko, Viliam (oponent)
Na rozdíl od komerčních komponentových systémů nemají ty akademické dostatečnou podporu v integrovaných vývojových prostředích. Tato práce analyzuje vývoj komponentově založených aplikací na komponentovém sys- tému SOFA 2 a zjišťuje, že hlavním problémem je nedostatečné propojení mezi procesy obecného návrhu aplikace a vytváření konkrétních komponent. Na základě této analýzy definuje podmnožinu UML, univerzálního jazyka pro návrh aplikací, a její sémantiku vzhledem k entitám komponentového systému SOFA 2. Dále vytváří nástroj integrovaný do vývojového prostředí Eclipse, který umožňuje automatické generování těchto entit z UML kom- ponentového modelu, stejně jako propojení tohoto modelu s již existujícími entitami, umožňující jejich automatickou opravu v případě změny modelu. Tento nástroj je navržen modulárně tak, aby bylo možné jednoduše změnit sémantiku modelu nebo ho použít na jiné modely. Nakonec tato práce ana- lyzuje možnosti rozšíření tohoto nástroje na další komponentové systémy, generování kódu a verifikaci chování komponent.
|
|
|
Hazardní hra ruleta
Vlk, Marek ; Malohlava, Michal (vedoucí práce) ; Šimko, Viliam (oponent)
Tato práce se věnuje hazardní hře ruletě. Jejím stěžejním cílem je navrhnout a implementovat tuto hru. Aplikace poskytuje dva režimy hraní: cvičná hra pracující o -line a skutená hra, která umožňuje hru o více hráčích on-line. Práce se zaměřuje na rychlost a spolehlivost síťové komunikace i na uživatelsky přívětivé 3D prostředí kasina. V programu je dále umožněno hraní a simulování herních systémů, které jsou implementovány, a lze importovat vlastní. Aplikace je napsána v jazyce C# pro platformu Windows. Síťová komunikace je uskutečněna pomocí technologie .NET Remoting.
|
|
|
Multimedia Grid
Šimko, Viliam
Práce popisuje současné možnosti a problémy videokonferenčních systémů se zaměřením na volně dostupné technologie určené pro group-to-group komunikaci. Úvod práce obsahuje popis vybraných komerčních i volně dostupných systémů. Pozornost je soustředěna na technologii AcessGrid, která využívá multicastovou síť pro doručování multimediálních dat. V práci je popsaný AccessGridový uzel v organizaci CIANT, který se stal východiskem pro návrh architektury uzlu založeného čistě na volně dostupných komponentách s otevřeným zdrojovým kódem, konkrétně AccessGrid pro platformu Linux. Jedna z kapitol je věnována i problémům spojených s překonáváním firewallu a NAT a porovnání kodeků a protokolů používaných při videokonferenčním přenosu. Závěr práce se dotýká archivace konference, s čímž souvisí i vytvoření nového nástroje StreamVNC určeného pro lokální nahrávání a přípravu prezentací. Ten využívá nástroj AGVCR pro nahrávání RTP paketů, které vznikají snímáním VNC obrazovky a obrazu z kamery pomocí aplikace EVIC a kódováním zvuku aplikací RAT.
|
|
|
Multimedia Grid
Šimko, Viliam ; Galamboš, Leo (vedoucí práce) ; Jirovský, Václav (oponent)
The thesis describes the possibilities and issues of existing videoconferencing systems. We focus on open-source solutions for group-to-group communication especially the AccessGrid technology that utilizes the multicast packet delivery method of multimedia content. We describe AccessGrid node created for CIANT organization, which has been taken as a starting point for de ning the architecture of a videoconferencing system based exclusively on open-source components, particularly Linux and related software. We address issues related to rewalls and NAT traversal and provide a comparison of various videoconference-related codecs and protocols. Finally, the text touches the question of recording and archiving of conference sessions and provides a new integrated recording application { StreamVNC. The tool allows users to prepare their presentations using localhost recording facility which includes AGVCR for recoding RTP packets, EVIC for grabbing the VNC display and camera source and RAT as an audio encoder.
|
|
|
Syntax-based extraction of component behavior specifications
Reidinger, Josef ; Šimko, Viliam (oponent) ; Poch, Tomáš (vedoucí práce)
Pro velké softwarové systémy je možné použít komponentový způsob vývoje. Jeho výhody jsou, že lze snadno části použít opakovaně a pokud obsahuje i popis chování, tak lze systém snadněji analyzovat. Komponenty jsou tvořeny popisem rozhraní a volitelně popisem chovaní. Popis chování je možné zkoumat na porušení omezení jiných komponent při jejich použití, jestli chování je očekávané a jestli komponenty k sobě pasují. Popis chování definuje omezení použítí komponenty a jak reaguje na zavolaní každé své poskytované metody. Reakce popisuje pořadí a četnost volání metod požadovaných komponent. Manuální definování chovaní komponenty je náchylné k chybám a mělo by se zautomatizovat. Výsledkem této práce je nástroj který z kódu, který splňuje omezení, je schopen vygenerovat automaticky popis chování. Nástroj je možné použít pro automatické generování popisu chování při převodu běžného softwaru na komponenty nebo při úpravě komponenty ke kontrole změny chování změnené komonenty. Práce také obsahuje prozkoumání možných technologií využitelných pro analýzu. Nástroj je součástí mezinárodního Q-Impress projektu a využívá jeho nástroje pro svoji funkci a naopak.
|
host ::
RSS.