|
|
Fighting the State Explosion Problem in Component Protocols
Holub, Viliam ; Plášil, František (vedoucí práce) ; Brada, Přemysl (oponent) ; Reussner, Ralf H. (oponent)
In complex software component systems, it is desirable to verify the correctness of the composition before deployment. To achieve a trustworthy composition, the behavior of components is formally described and the composition is veri ed against communication errors. Unfortunately, the number of states of a model tends to grow exponentially with the size of the model's description | the state explosion problem. Because the exhaustive veri cation has to visit all the states of the model, the veri cation leads to unacceptable space and time requirements. In this thesis, we present several approaches to cope with the state explosion problem in behavior protocols. First, we reduce a size of the speci cation by enhancing the speci cation language by exceptions and, additionally, we reduce the speci cation by symbolic manipulations with respect to composition. Then, we present a novel approach to distributed veri cation, which involves external storage devices. Finally, we reduce the number of states, which have to be traversed by identifying representatives in the state space.
|
|
| |
|
|
Refinement of timed automata models according to hardware characteristics
Hamrle, Martin ; Kofroň, Jan (oponent) ; Holub, Viliam (vedoucí práce)
Timed automata byla navržena na modelování real-time systémů. Formální teorie obsahuje některé nerealistické předpoklady, například nekonečně rychlé akce. Model pak musí toto chování namodelovat, což ale znepřehledňuje celý model, a tím je celé modelování náchylnější k chybám. V předložené práci se zaměříme na synchronizaci procesů pomocí kanálů. Diskutují se jednotlivé možnosti řešení zpoždění signálů. Poté následuje analýza vybraných řešení a jejich implementace. Nevytváří se nový nástroj a jazyk, ale vytváří se pouze rozšíření současného jazyka, aby bylo možné použít grafi cké prostředí nástroje Uppaal.
|
|
|
Využití simulačních a výpočtových prostředí ve výuce fyziky
Dekar, Martin ; Babka, Vlastimil (oponent) ; Holub, Viliam (vedoucí práce)
Předložená práce se zabývá problematikou tvorby interaktivních fyzikálních simulací (současného trendu v e-learningu) z pohledu programátora. Úvod práce čtenáři představuje interaktivní výukovou simulaci a poskytuje vodítka pro výběr vývojového prostředí vhodného k tvorbě většího množství takovýchto simulací. Práce dále podrobněji rozebírá čtyři existující vývojové nástroje, ověřuje jejich vhodnost implementací reálné úlohy - tlumeného harmonického oscilátoru a tuto implementaci popisuje. Dále je v práci představena vzdělávací simulace většího rozsahu, implementovaná v prostředí Adobe Flash CS3, která představuje nový směr v e-learningu - možností získání datových výstupů, kterým se simulace blíží skutečnému experimentu. K této simulaci patří i knihovna více než stovky gra ckých objektů znovupoužitelných při tvorbě dalších simulací. Práci uzavírá kritické zhodnocení výsledk· a naznaení východisek pro dalí práci.
|
|
|
Creating Panoramic Images from Photographs Acquired with Different Camera Settings
Fibichr, Jaroslav ; Holub, Viliam (oponent) ; Sedlář, Jiří (vedoucí práce)
Při fotografování scény za účelem vytváření panoramatických snímků bývá vhodnější upravit nastavení fotoaparátu pro každou fotografii zvlášt, aby zůstalo zachováno spráné rozložení jasů. V takovém souboru obrázků pro panorama však bývají mezi spojovanými snímky velké jasové rozdíly. Cílem této práce je navrhnout řešení, které by rozdíly mezi snímky potalčilo a implementovat jej v programu Panomedic. První metoda je založena na přímém mapování jasových hodnot v překrývajících se částech snímků. Druhá metoda využívá statistických hodnot získaných z rozdělení jasů ve snímcích. Dále je popsána metoda pro hledání hranice mezi jednotlivými snímky použitá pro spojovíní. Výsledkem je panoramatická fotografie bez viditelných přechodů mezi zdrojovými snímky.
|
|
|
Robot navigation on the chessboard
Mikulík, Andrej ; Ježek, Pavel (oponent) ; Holub, Viliam (vedoucí práce)
Predložená práca sa zaoberá lokalizáciou mobilného robota. Lokalizácia je postavená na počítačovom videní. Zo snímaného obrazu navrhnuté algoritmy rozpoznávajú šachovnicovú podložku, po ktorej sa robot pohybuje. Pomocou nej je analyzovaný uhol natočenia a pozícia robota. Navrhnutý algoritmus bol otestovaný a zhodnotený na reálnom robotovi.
|
|
|
Combining bracketed pictures
Roubíčková, Anna ; Adámek, Jiří (oponent) ; Holub, Viliam (vedoucí práce)
Světelný rozsah fotografovaných scén je často větší, než je digitální fotoaparát schopen zachytit. Tento problém bývá řešen několikanásobným vyfotografováním záběru s rozdílnými expozicemi (bracketing). Tato práce představuje program ImageLighter, který automaticky kombinuje sérii fotografií téže scény tak, aby obnovil její původní dynamický rozsah. Při kombinování algoritmus využívá veškerou dostupnou obrazovou informaci. Výsledek by tedy měl zachycovat počáteční rozložení jasu věrněji. Práce popisuje použité algoritmy a datové struktury a poskytuje srovnání s konkurenčními přístupy.
|
|
|
Forensic RAM dump image analyzer
Kollár, Ivor ; Holub, Viliam (vedoucí práce) ; Děcký, Martin (oponent)
Pro získávání obrazů operační paměti počítače existují různé techniky, většina z nich ala poskytuje syrový obraz dat, který je obtížné analyzovat. Cílem téhle práce je vyvinout program pro automatickou analýzu obrazů paměti poskytující obsažené informace v uživatelsky přívětivé formě. Program by měl zjednodušit automatické dolování dat a předpokládaným uživatelem jsou forenzní znalci. Předpokládané technické schopnosti jsou podpora vícero architektur a operačních systémů, hádání cílové architektury a operačního systému, automatické získávání hesel a šifrovacích klíčů, vypsání seznamu procesů, modulů, ovladačů.
|
|
|
Steganographics filesystem
Kollár, Ivor ; Parízek, Pavel (oponent) ; Holub, Viliam (vedoucí práce)
V predloženej práci študujeme možnosti ochrany informácie v situácii, keď samotná kryptogra a nestačí. Skúsime rozobrať možnosť utajenia informácie, nie však v nevinne sa tváriacom nosiči( zvuk, obraz, video ), ale v pseudosteganografi ckom archíve. Pokúsime sa popísať, a neskôr aj implementovať algoritmus, ktorý bude schopný vytvoriť archív, spájajúci nasledujúce vlastnosti: Bude obsahovať N súborov, každý chránený jedným z N klúčov, pričom číslo N sa pokúsime útočníkovi zatajiť. Pri použití jedného z klúčov získame práve jeden súbor, pričom o existencii ostatných súborov by sme nemali získať žiadnu informáciu. Implementácia tohto algoritmu by mala byť čo najjednoduchšia, platformovo čo najmenej závislá, a jednoducho prakticky použitelná.
|
|
|
FTP server
Tekeľ, Michal ; Holub, Viliam (oponent) ; Štanclová, Jana (vedoucí práce)
Práca sa zaoberá implementáciou efektívneho FTP servra a programov potrebných na jeho správu, ktoré sú jej súčasťou. Dôležitým kritériom je výkon a schopnosť plne využívať dostupné prostriedky v prípade potreby. Server má podporovať všetky bežné FTP príkazy, menej používané umožňuje doplniť pomocou pluginov. Dielom práce je aj komunikačný protokol medzi servrom a administrátorskými programami, ktorý umožňuje správu aj pomocou cudzích programov.
|
host ::
RSS.