|
|
Model Checking Infinite-State Systems Using Language Inference
Rozehnal, Pavel ; Křena, Bohuslav (referee) ; Vojnar, Tomáš (advisor)
Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We implement regular model checking using inference of regular languages. The method builds upon the observations that for infinite-state systems whose behavior can be modeled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations. Our new approach to regular model checking via inference of regular languages is based on the Angluin's L* algorithm that is used for finding out an invariant which can answer our question whether the system satisfies some property. We also provide an intro to the theory of finite automata, model checking, SAT solving and Anguin's L* and Bierman algorithm of learning finite automata.
|
|
|
Search of Control Strategies Using UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (referee) ; Strnadel, Josef (advisor)
This thesis deals with finding control strategies for pre-selected problems from various areas using tool Uppaal Stratego. Four areas were selected, namely chess, a sliding puzzle, the tower of Hanoi, and a kinematic problem involving a package, a car, and an airplane. For the selected areas and problems, a set of models was designed and implemented. For the tower of Hanoi and the sliding field, it was possible to successfully evaluate relevant strategies, raising the probabilities of success to more than 90 %. For other models, a problem was found in the size of the state space and the strategies could not be evaluated because the maximum memory capacity that the tool uses was not sufficient. For the kinematic problem, after limiting and simplifying the model, the strategies were successfully evaluated, but for chess, this was not possible even after significant simplification.
|
|
|
Specifications Database of Security Protocols
Ondráček, David ; Trchalík, Roman (referee) ; Očenášek, Pavel (advisor)
Original protocols, which were created during early development of computer networks, no longer provide sufficient security. This is the reason why new protocols are developed and implemented. The important component of this process is formal verification, which is used to analyze the developed protocols and check whether a successful attack is possible or not. This thesis presents selected security protocols and tools for their formal verification. Further, the selected protocols are specified in LySa calculus and results of their analysis using LySatool are presented and discussed.
|
|
|
A VHDL Parser for Formal Verification
Matyáš, Jiří ; Smrčka, Aleš (referee) ; Charvát, Lukáš (advisor)
The principal goal of this bachelor thesis is to design and implement a parser of VHDL language into graph representation in VAM (Variable Assignment Language). The application is developed for formal verification purposes of VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The development of the compiler described in this thesis should provide the opportunity to use formal verification techniques to verify hardware designs described in high level design languages, such as VHDL.
|
|
| |
|
|
Verification of Programs with Pointers Based on Pattern Detection
Kubíček, Jan ; Erlebach, Pavel (referee) ; Vojnar, Tomáš (advisor)
This paper presents our results in study of verifiaction of infinite state space systems. We deal more concretely with abstract model checking. As main part of study we learned about pattern-based verification. This method is supposed to verify programs with dynamic memory structures like lists. Those structures are presented as directed graph. Pattern-based verifiaction abstracts any number of nodes by replacing them with summarized node. This way we achieve bounded presentation of unbounded memory structure. Afterwards, verification is very effective due to low number of possible memory configurations. In our own work we deal with making model of a program for a tool that implements pattern-based verification. This model isconstructed from a subset of the C language. The main contribution of work is making the verification of simple programs written in C language completely self-acting by automation of constructing input model. In this paper wepresent the grammar of created subset of the C language and implementation details of translation.
|
|
|
Verification of Pointer Programs Based on Forest Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Holík, Lukáš (advisor)
In this work, we focus on improving the forest automata based shape analysis implemented in the Forester tool. This approach represents shapes of the heap using forest automata. Forest automata are based on tree automata and Forester currently has only a simple implementation of tree automata. Our first contribution is replacing this implementation by the general purpose tree automata library VATA, which contains the highly optimized implementations of automata operations. The version of Forester using the VATA library participated in the competition SV-COMP 2015. We further extended the forest automata based verification method with two new techniques - a counterexample analysis and predicate abstraction. The first one allows us to determine whether a found error is a real or spurious one. The results of the counterexample analysis is also used for creating new predicates which are used for the refinement of predicate abstraction. We show that both of these techniques contribute to an improvement over the early approach.
|
|
|
An Efficient Finite Tree Automata Library
Lengál, Ondřej ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.
|
|
| |
|
|
Enriching the Process of Verification of RISC-V Processor with Formal Techniques
Horký, Jakub ; Šnobl, Pavel (referee) ; Hruška, Tomáš (advisor)
This thesis provides a brief overview of the RISC-V architecture, design of processors, and how easily a bug can arise during the development. Then this thesis describes the way functional verification tries to discover those bugs and what are its pros and cons. More specifically, the thesis focuses on what the verification environment in UVM look like. Then the thesis describes, how formal verification fits in to the functional verification and shows the tools that are available for formal verification. The final part of this thesis, describes the process of how I wrote the assertions (written in SVA) for a RISC-V processor, using a property checking tool. Using these assertions for verifying a processor in the late stage of development, when functional verification already had the possibility to discover most of the bugs, I still was able to discover few of those bugs.
|
guest ::
