|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
Generování stromových struktur pro účely testování informačních systémů
Rozsíval, Michal ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této práce je vytvořit nástroj automatizující testování informačních systémů. Nástroj vytváří testovací zprávy podobné těm v reálném provozu, přičemž podobností se v rámci této práce rozumí podobnost struktur posílaných dat. Princip činnosti spočívá ve zpracování záznamu komunikace, který si nástroj načte a jednotlivé v něm obsažené zprávy převede do uniformního formátu. Takto uložené zprávy klasifikuje do skupin, které abstrahuje do podoby vhodné pro následné generování náhodných testovacích zpráv. Podporována je komunikace prostřednictvím protokolu REST API a OPC UA a stromově strukturovaná data ve formátu JSON a XML . Nové zprávy jsou vytvářeny na základě kombinačního testování s pokrytím Pair-Wise . Výsledná funkcionalita nástroje byla ověřena na reálných záznamech komunikace.
|
|
|
Automatizovaná detekce datových typů ve strukturách
Oháňka, Martin ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá syntézou datových struktur pro účely testování softwaru. Konkrétně se práce věnuje analýze reálných dat za účelem detekce datových typů pro následné generování testovacích dat. Analýza dat je prováděna ve dvou rovinách: řídícím systémem pro plánování a spouštění dílčích detekcí a samotnými detektory. Výsledkem této bakalářské práce je analýza a implementace nástroje obsahující sadu detektorů datových typů nad stromovými datovými strukturami jako jsou JSON, YAML či XML. Detektory mají za úkol určit význam hodnot, případně i závislosti mezi daty. Sadu lze podle potřeby snadno rozšířit, aby bylo možné detekovat i složitější významy a závislosti. Výsledky těchto analýz půjde využít pro generovaní nových testovacích dat pro účely testování softwaru.
|
|
|
Efektivní funkcionální knihovna pro konečné automaty
Říha, Jakub ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
Konečné automaty jsou důležitou matematickou abstrakcí. Ve formální verifikaci se konečné automaty používají ke stručné reprezentaci regulárních jazyků. V této souvislosti se používají operace nad konečnými automaty, jako je testování jazykové univerzality a inkluze. Naivní přístup k implementaci těchto operací vede k explicitní determinizaci konečného automatu, což může být nakladné a nežádoucí. Nicméně existuje pokročilejší metoda k vykonávání těchto operací nazývaná Antichains algoritmus, která se vyhýbá explicitní determinizaci. Tato práce se zabývá efektivní implementací operací nad konečnými automaty v Haskellu a také porovnává několik implementačních variant. Získané výsledky jsou poté porovnány s knihovnou VATA, což je imperativní implementace knihovny pro práci nad konečnými automaty.
|
|
|
Efektivní algoritmy pro stromové automaty
Valeš, Ondřej ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je navržení efektivních algoritmů pro testování jazykové ekvivalence a inkluze stromových automatů a dále pak implementace těchto algoritmů jako rozšíření knihovny VATA. Nejprve je provedena rešerše existujících přístupů testování ekvivalence a inkluze slovních i stromových automatů. Z nich poté vychází návrh nového přístupu k testování ekvivalence a inkluze jazyků stromových automatů založený na bisimulaci vzhledem ke kongruenci, ke kterému je představen formální důkaz korektnosti. Součástí práce je také srovnání efektivity představeného algoritmu a již existujících přístupů, které ukazuje, že na obtížných případech je náš algoritmus často lepší než existující přístupy.
|
|
|
Bezdrátová senzorová síť
Hruška, Martin ; Burda, Karel (oponent) ; Mišurec, Jiří (vedoucí práce)
Bezdrátové senzorové sítě (WSN) se skládají z kombinace několika výkonných zařízení (označovaných jako „base stations“ nebo „sink“, dále základna) a velkého počtu (1000 - 1000000) levných zařízení (označovaných jako „nodes“, dále uzly) s extrémně omezenou výpočetní sílou, pamětí a energií. Jednotlivé uzly jsou vybaveny snímačem okolního prostředí. Data zaznamenaná snímači jsou lokálně předzpracována a poté zasílána základně k dalšímu zpracování. Využití WSN je očekáváno v široké škále oblastí. Cílem práce je rozebrat možnosti realizace bezdrátového přenosu digitalizovaných údajů ze senzorů. Práce zahrnuje a srovnává: Wi – Fi, WiMAX, ZigBee, GPRS, rádiovou síť a IrDA. Navrhne se bezdrátová síť pro sběr dat z čidel domácí čističky odpadních vod na území malé vesnické aglomerace s přenosem dat do centrálního dispečinku. Navrhne se několik alternativ a porovnají se jejich vlastnosti a možnosti.
|
|
|
Podpora průběžné integrace v rámci systému Copr
Klusoň, Martin ; Hruška, Martin (oponent) ; Rogalewicz, Adam (vedoucí práce)
Práce se zabývá implementací průběžné integrace pro build systém Copr. Implementace využívá framework Citool a jeho moduly, které se již používají pro průběžnou integraci build systému Koji. Výsledný systém umožňuje automaticky spustit testování pro nový balíček v build systému Copr a otestovat ho v prostředí virtuálního stroje. Práce ukazuje způsob, jakým je možné realizovat průběžnou integraci pro build systém Copr.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
A Web Interface for the Management of Virtual Portfolio
Bali, Filip ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis designs and implements a web application for managing virtual portfolios. Main goal of the application is visualise and analyze data from stock exchange services API. User can be notified on price change. The application also uses existing methods to predict stock prices and supports the visualization of the user's stock exchange decisions and provides him/her a general overview of them.
|
|
|
Knihovna pro konečné automaty a převodníky
Bieliková, Michaela ; Lengál, Ondřej (oponent) ; Hruška, Martin (vedoucí práce)
Konečné automaty majú široké uplatnenie v informatike, okrem iných vo formálnej verifikácii, modelovaní systémov a spracovaní prirodzeného jazyka. Avšak modely skutočne reprezentujúce realitu bývajú veľmi komplikované a môžu byť definované nad veľkými, v niektorých prípadoch až nekonečnými, abecedami, a teda môžu obsahovať veľký počet prechodov. V týchto prípadoch nemusí byť je použitie algoritmov na prácu s konečnými automatmi efektívne. Symbolické automaty poskytujú stručnejší zápis tak, že namiesto symbolov v prechodoch používajú predikáty. Konečné prevodníky tiež majú široké uplatnenie, od ligvistiky až po formálnu verifikáciu. Symbolické prevodníky nahradzujú symboly dvojicou predikátov - jeden predikát pre vstupné symboly a jeden pre výstupné. Cieľom tejto práce je návrh knižnice pre klasické a symbolické automaty a prevodníky, ktorá bude vhodná na rýchle prototypovanie nových algoritmov.
|
host ::
RSS.