|
|
Library for Finite Automata and Transducers
Bieliková, Michaela ; Lengál, Ondřej (referee) ; Hruška, Martin (advisor)
Finite state automata are widely used in the field of computer science such as formal verification, system modelling, and natural language processing. However, the models representing the reality are complicated and can be defined upon big alphabets, or even infinite alphabets, and thus contain a lot of transitions. In these cases, using classical finite state automata is not very efficient. Symbolic automata are more concise by employing predicates as transition labels. Finite state transducers also have a wide range of application such as linguistics or formal verification. Symbolic transducers replace classic transition labels with two predicates, one for input symbols and one for output symbols. The goal of this thesis is to design a library for letter and symbolic automata and transducers which will be suitable for fast prototyping.
|
|
|
Incremental Inductive Coverability for Alternating Finite Automata
Vargovčík, Pavol ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
In this work, we propose a specialization of the inductive incremental coverability algorithm that solves alternating finite automata emptiness problem. We experiment with various design decisions, analyze them and prove their correctness. Even though the problem itself is PSpace-complete, we are focusing on making the decision of emptiness computationally feasible for some practical classes of applications. We have obtained interesting comparative results against state-of-the-art algorithms, especially in comparison with antichain-based algorithms.
|
|
|
Control System for an Automatic Assembly Line
Jakeš, Libor ; Beran,, Jan (referee) ; Hynčica, Ondřej (advisor)
This master’s thesis deals with programming of control system for an automatic assembly line rear seats of passenger cars. The theoretical part describes assembly line, PLC, robot, electric nutrunner and intelligent camera Sick. Practical part of the thesis characterizes created programs of assembly workplace control system. This part also explains creating a model of station and subsequent formal verification of basic safety and functional properties.
|
|
|
Feedback Hardware Functional Verification
Santa, Marek ; Kajan, Michal (referee) ; Kořenek, Jan (advisor)
In the development process of digital circuits, it is often not possible to avoid introducing errors into systems that are being developed. Early detection of such errors saves money and time. This project deals with automation of feedback in functional verification of various data processing components. The goal of automatic feedback is not only to shorten the time needed to verify the functionality of a system, but mainly to improve verification coverage of corner cases and thus increase the confidence in the verified system. General functional and formal verification principles and practices are discussed, coverage metrics are presented, limitations of both techniques are mentioned and room for improvement of current status is identified. Design of feedback verification environment using a genetic algorithm is described in detial. The verification results are summarized and evaluated.
|
|
|
Questa Capabilities Demonstration Set
Krajčír, Stanislav ; Kajan, Michal (referee) ; Zachariášová, Marcela (advisor)
This bachelor thesis deals with presentation of capabilities of verification platform Questa Static from Mentor Graphics company. The basic information about the principles of assertion based verification is provided in the beginning. The thesis describes Questa AutoCheck verification tool which is used for automatic verification of integrated circuits and Questa Formal verification tool which is used for static formal verification of integrated circuits. The set of examples is given to demonstrate various options of using these tools for verification of a concrete integrated circuit design. In conclusion, the thesis evaluates the possibilities of application of these tools in verification process.
|
|
|
Program Instrumentation Enabling Coverage Measurement in SW Testing
Kapoun, Petr ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This work deals with the design and creation of an instrumentation tool for measuring coverage in software testing. During compilation, the tool obtains a representation of selected parts of the program in the form of a control flow graph and instruments the given parts of the program by inserting function callbacks. Using the data generated when calling the function callbacks of the instrumented program, the tool evaluates the measurement of the coverage criteria. Supported coverage criteria include line coverage and selected control flow and data flow coverage criteria.
|
|
|
A Decision Procedure for the WSkS Logic
Fiedor, Tomáš ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
Různé typy logik se často používají jako prostředky pro formální specifikaci systémů. Slabá monadická logika druhého řádu s k následníky (WSkS) je jednou z nich a byť má poměrně velkou vyjadřovací sílu, stále je rozhodnutelná. Ačkoliv složitost testování splnitelnosti WSkS formule není ani ve třídě ELEMENTARY, tak existují přístupy založené na deterministických automatech, implementované např. v nástroji MONA, které efektně řeší omezenou třídu praktických příkladů, nicméně nefungují pro jiné. Tato práce rozšiřuje třídu prakticky řešitelných příkladů, a to tak, že využívá nedávno vyvinutých technik pro efektní manipulaci s nedeterministickými automaty (jako je například testování universality jazyka pomocí přístupu založeného na antichainech) a navrhuje novou rozhodovací proceduru pro WSkS využívající právě nedeterministické automaty. Procedura je implementována a ve srovnání s nástrojem MONA dosahuje v některých případech řádově lepších výsledků.
|
|
|
Security of Contactless Smart Card Protocols
Henzl, Martin ; Rosa, Tomáš (referee) ; Staudek, Jan (referee) ; Hanáček, Petr (advisor)
Tato práce analyzuje hrozby pro protokoly využívající bezkontaktní čipové karty a představuje metodu pro poloautomatické hledání zranitelností v takových protokolech pomocí model checkingu. Návrh a implementace bezpečných aplikací jsou obtížné úkoly, i když je použit bezpečný hardware. Specifikace na vysoké úrovni abstrakce může vést k různým implementacím. Je důležité používat čipovou kartu správně, nevhodná implementace protokolu může přinést zranitelnosti, i když je protokol sám o sobě bezpečný. Cílem této práce je poskytnout metodu, která může být využita vývojáři protokolů k vytvoření modelu libovolné čipové karty, se zaměřením na bezkontaktní čipové karty, k vytvoření modelu protokolu a k použití model checkingu pro nalezení útoků v tomto modelu. Útok může být následně proveden a pokud není úspěšný, model je upraven pro další běh model checkingu. Pro formální verifikaci byla použita platforma AVANTSSAR, modely jsou psány v jazyce ASLan++. Jsou poskytnuty příklady pro demonstraci použitelnosti navrhované metody. Tato metoda byla použita k nalezení slabiny bezkontaktní čipové karty Mifare DESFire. Tato práce se dále zabývá hrozbami, které není možné pokrýt navrhovanou metodou, jako jsou útoky relay.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Instrumentation of C/C++ Programs during Compilation
Mušková, Kateřina ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This thesis presents design and implementation of the TforcTool offering compile-time instrumentation of memory access and functions. The tool is built on an existing static instrumenting tool Tforc, which was extended in order to provide greater usability and functionality. The advantage of this solution compared to another compile-time tools is that there is no need to change current compile structure of project.
|
guest ::
