|
|
A Decision Procedure for the WSkS Logic
Fiedor, Tomáš ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Various types of logics are often used as a means for formal specification of systems. The weak monadic second-order logic of k successors (WSkS) is one of these logics with quite high expressivity, yet still decidable. Although the complexity of checking satisfiability of a WSkS formula is not even in the ELEMENTARY class, there are approaches to this problem based on deterministic tree automata that perform well in practice, like the MONA tool that efficiently solves the class of practical formulae, but fails for some others. This work extends the class of practically solvable formulae with the use of recently developed techniques for efficient manipulation of non-deterministic automata (such as the antichains algorithm for testing universality) and designs a new decision procedure using non-deterministic automata. The procedure is implemented and is compared with the MONA tool and for some cases yield better results than MONA.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Databáze specifikací bezpečnostních protokolů
Ondráček, David ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Původní protokoly, které vznikaly v počátcích vývoje počítačových sítí, již nejsou pro zajištění potřebné bezpečnosti dostačující. Proto se stále vyvíjejí a implementují protokoly nové. Důležitou součástí tohoto procesu je formální verifikace. Jde o analýzu protokolu po formální stránce, kdy se zjišťuje, zda lze protokol úspěšně napadnout. Diplomová práce se zabývá analýzou vybraných bezpečnostních protokolů a nástrojů pro jejich formální verifikaci. Výstupem praktické části je databáze specifikací protokolů v LySa kalkulu a výsledky jejich verifikace nástrojem LySatool.
|
|
|
Překladač jazyka VHDL pro potřeby formální verifikace
Matyáš, Jiří ; Smrčka, Aleš (oponent) ; Charvát, Lukáš (vedoucí práce)
Cílem této bakalářské práce je navrhnout a implementovat překladač, který umožňuje převod popisu hardware z jazyka VHDL do grafové reprezentace v jazyce VAM (Variable Assignment Language). Program je určen pro potřeby formální verifikace výzkumné skupiny VeriFIT Fakulty informačních technologií VUT Brno. Důvodem vypracování této práce je poskytnutí možnosti formálně verifikovat návrh hardware s využitím vysokoúrovňových návrhových jazyků, jakým je například jazyk VHDL.
|
|
|
Řídicí systém pro automatické montážní pracoviště
Jakeš, Libor ; Beran,, Jan (oponent) ; Hynčica, Ondřej (vedoucí práce)
Tato diplomová práce se zabývá naprogramováním řídicího systému pro automatizované montážní pracoviště zadních opěradel do osobních aut. V teoretické části je popis stanoviště, PLC, robota, elektrický utahováku a inteligentní kamery Sick. V praktické části jsou popsány vytvořené programy řídicího systému automatizovaného stanoviště. Dále je ještě v praktické části vysvětleno vytvoření modelu stanoviště a následné provedení formální verifikace základních bezpečnostních a funkčních vlastností.
|
|
|
Slicing specifikace chování komponent
Šerý, O. ; Plášil, František
Specifikace chování umožňuje reuse nejen komponent, ale také komponentové architektury. V takovém případě je ovšem velmi obtížné určit, jaké je skutečné chování komponenty, neboť toto silně závisí na kontextu. V tomto článku popisujeme metodu slicingu behavior protokolů, která umožňuje automaticky určit chování komponenty v daném prostředí.
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Přestože existuje několik model checkerů pro software, které ověřují kód proti specifikaci zapsané např. v temporální logice a tzv. assertions, nebo ověřují nízkoúrovňové vlastnosti (jako neošetřené výjimky), žádný z nich nepodporuje ověřování softwarových komponent proti vyšší specifikaci chování. Tato zpráva popisuje náš přístup k model checkingu softwarových komponent implementovaných v jazyce Java proti specifikaci jejich chování definované pomocí protokolů chování, který využívá model checker Java PathFinder a protocol checker. Vlastnosti ověřované nástrojem Java PathFinder (korektnost sekvencí volání metod) se validují pomocí spolupráci s nástrojem protocol checker. Ukazujeme, že pouze návrhový vzor publisher/listener, označovaný za klíčový pro podporu rozšiřitelnosti v nástroji Java PathFinder, nebyl dostatečný pro tento typ ověřování (přestože byl pro nás velmi užitečný).
|
|
|
Rozšíření Behavior Protocols o data a multisynchronizaci
Kofroň, Jan
Použití Behavior Protocols pro specifikaci chování komponent v hierarchických komponentových modelech (SOFA, Fractal) se ukázalo být vhodným přístupem, pokud nás zajímá absence komunikačních chyb mezi komponentami v dané aplikaci. Během specifikace Fractalové komponentové aplikace zaměřené na kontrolu přístupu k internetu na letištích umožňující několik způsobů úhrady se projevilo několik nedostatků Behavior Protocols jako specifikační platformy. Dvě nejdůležitější zahrnují (i) nedostatečná vyjadřovací síla Behavior Protocols při specifikaci některých běžných vzorů chování a (ii) nedostatečný výkon aplikace Behavior Protocol Checker – nástroje použitého pro hledání kompozičních chyb mezi komunikujícími komponentami. Tento článek se soustředí na řešení prvního problému pomocí rozšíření formalismu Behavior Protocols.
|
|
|
Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Kofroň, Jan
Používání softwarových komponent patří k moderním přístupům k vytváření rozšiřitelných a spolehlivých aplikací. K zajištění vysoké spolehlivost by komponentová aplikace měla být verifikována, např. podstoupit model checking. Implementace aplikace je většinou příliš složitá, než aby mohla být verifikována na formální úrovni. Proto se používá model, který je abstrakcí této implementace. Behavior Protocols jsou platformou pro modelování chování softwarových komponent. V tomto článku navrhujeme metodu pro překlad specifikace Behavior Protocols do Promely, která je následně použita jako vstup pro model checker Spin. Pokud máme model v jazyku Promela popisující chování komponent, můžeme efektivně ověřovat kompatibilitu i LTL vlastnosti kooperujících komponent.
|
host ::
RSS.