|
|
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.
|
|
|
Inkrementální induktivní pokrytelnost pro alternující konečné automaty
Vargovčík, Pavol ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
V tejto práci navrhujeme špecializáciu algoritmu inductive incremental coverability, ktorá rieši problém prázdnosti alternujúcich konečných automatov. Experimentujeme s rôznymi návrhovými rozhodnutiami, analyzujeme ich a dokazujeme ich korektnosť. Aj keď je známe, že problém je sám o sebe PSpace-ťažký, zameriavame sa na to, aby bolo rozhodovanie prázdnosti výpočetne prijateľné v niektorých triedach automatov s praktickým využitím. Dosiahli sme niekoľko zaujímavýcch výsledkov v porovnaní so špičkovými algoritmami, predovšetkým v porovnaní s algoritmami založenými na protireťazcoch.
|
|
|
Ří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í.
|
|
|
Zpětnovazební funkční verifikace hardware
Santa, Marek ; Kajan, Michal (oponent) ; Kořenek, Jan (vedoucí práce)
Vyhnout se chybám při vývoji číslicových systémů je téměř nemožné. Přitom brzké odhalení chyb pomáha šetřit čas i peníze. Tato práce se zabývá automatizací zpětné vazby ve funkčních verifikacích různých komponent na spracování dat. Automatická zpětná vazba má za úkol přinést nejen zkrácení času potřebného k ověření funkčnosti systému, ale zejména zlepšit prohledávání okrajových podmínek a zvýšit tak důvěru ve verifikovaný systém. V práci jsou diskutovány principy a postupy jak funkční tak i formální verifikace, metriky poskytující představu o tom, jaká část funkcionality byla pokryta, jsou popsány nedostatky zmíněných technik a identifikován prostor pro zlepšení současného stavu. Následně je představen návrh spětnovazebního verifikačního prostředí využívajícího genetický algoritmus. Na závěr práce jsou shrnuty dosažené výsledky verifikace.
|
|
|
Sada příkladů pro demonstraci práce s platformou Questa
Krajčír, Stanislav ; Kajan, Michal (oponent) ; Zachariášová, Marcela (vedoucí práce)
Tato bakalářská práce se zabývá prezentací práce s verifikační platformou Questa od společnosti Mentor Graphics při verifikaci číslicových obvodů. V úvodu práce jsou poskytnuty základní informace o principech verifikace založené na formálních tvrzeních. V rámci práce je uveden popis verifikačního nástroje Questa AutoCheck, který slouží k automatické kontrole obvodů a verifikačního nástroje Questa Formal, který slouží statické formální verifikaci číslicových obvodů. Na sadě příkladů užití jsou demonstrovány jednotlivé možnosti využití nástrojů při verifikaci konkrétního číslicového obvodu. V závěru práce jsou vyhodnoceny možnosti aplikace těchto nástrojů v praxi.
|
|
|
Instrumentace programů pro měření pokrytí při testování SW
Kapoun, Petr ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a tvorbou instrumentačního nástroje pro měření pokrytí při softwarovém testování. Nástroj při překladu získá reprezentaci vybraných částí programu v podobě grafu toku řízení a instrumentuje dané části programu vložením zpětných volání funkcí. Pomocí dat generovaných při volání vložených funkcí instrumentovaného programu nástroj vyhodnotí měření kritérií pokrytí. Mezi podporovaná kritéria pokrytí patří pokrytí řádků kódu a vybraná kritéria pokrytí toku řízení a toku dat.
|
|
|
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.
|
|
|
Security of Contactless Smart Card Protocols
Henzl, Martin ; Rosa, Tomáš (oponent) ; Staudek, Jan (oponent) ; Hanáček, Petr (vedoucí práce)
This thesis analyses contactless smart card protocol threats and presents a method of semi-automated vulnerability finding in such protocols using model checking. Designing and implementing secure applications is difficult even when secure hardware is used. High level application specifications may lead to different implementations. It is important to use the smart card correctly, inappropriate protocol implementation may introduce a vulnerability, even if the protocol is secure by itself. The goal of this thesis is to provide a method that can be used by protocol developers to create a model of arbitrary smart card, with focus on contactless smart cards, to create a model of the protocol, and to use model checking to find attacks in this model. The attack can be then executed and if not successful, the model is refined for another model checker run. The AVANTSSAR platform was used for the formal verification, models are written in the ASLan++ language. Examples are provided to demonstrate usability of the proposed method. This method was used to find a weakness of Mifare DESFire contactless smart card. This thesis also deals with threats not possible to cover by the proposed method, such as relay attacks.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
|
Instrumentace C/C++ programů při překladu
Mušková, Kateřina ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje TforcTool sloužícího k instrumentaci programů napsaných v jazyce C++, a to instrumentaci přístupu do paměti a volání funkcí. Nástroj staví už na existujícím nástroji Tforc poskytující statickou instrumentaci při překladu, jehož funkcionalitu a použitelnost rozšiřuje. Velkou výhodou oproti stávajícím řešením nabízejícím instrumentaci při překladu je možnost použití nástroje bez změny stávajících překladových skriptů (např. Make).
|
host ::
RSS.