|
|
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ů.
|
|
|
Dynamic Data Race Detection and Self-Healing in Java Programs
Letko, Zdeněk ; Kolář, Dušan (referee) ; Vojnar, Tomáš (advisor)
Finding concurrency bugs in complex software is difficult. As a contribution to coping with this problem the thesis proposes an architecture for a fully automated dynamic detection and healing of data races and atomicity violations in Java. Two distinct algorithms for detecting of data races are presented. One of them is a novel algorithm called AtomRace which detects data races as a special case of atomicity violations. The healing is based on suppressing a recurrence of the detected problem and can be performed by introducing an additional synchronization or by legally influencing the Java scheduler. Basically forces certain parts of the code to be executed atomically. The proposed architecture uses bytecode instrumentation to be able to track and influence the execution. The architecture and algorithms were implemented and tested on multiple case studies.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
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.
|
|
|
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.
|
|
|
Slicing specifikace chování komponent
Šerý, O. ; Plášil, František
Being an important means of reducing development costs, behavior specification of software components facilitates reuse of a component and even reuse of a component’s architecture (assembly). However, since typically only a part of the components’ functionality is actually used in the new context, a significant part of the behavior specification may be superfluous. As a result, it may be hard to see (and filter out) the actual interplay among the components in their behavior specification. This paper targets the problem in the scope of behavior protocols [13]. It presents a technique for slicing behavior protocols with respect to a given context (composition), designed to remove the unused behavior from a behavior specification. The technique is based on a formal foundation, generic enough to support slicing with respect to a property expressed as a predicate. To demonstrate viability of the proposed approach, a positive experience with behavior specification slicing applied in real-li
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1 which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking.
|
|
|
Rozšíření Behavior Protocols o data a multisynchronizaci
Kofroň, Jan
Using behavior protocol for behavior specification of components in hierarchical components model (SOFA, Fractal) turned out to be very beneficial if one is interested in communication errors among the application components. Recently, during specification of a Fractal component application aimed at controlling the access to the Internet at airports allowing for several types of payments for the access, several issues regarding the behavior protocols as a specification platform have arisen. The two most important are (i) insufficient expensiveness of behavior protocol language when specifying some typical behavior patterns, and (ii) insufficient performance of the behavior protocol checker – a tool used for searching for composition errors among communicating components. This paper focuses on solution of the first issue by proposing several extensions to behavior protocols.
|
|
|
Ověřování softwarových komponent: O překladu Behavior Protocols do Promely
Kofroň, Jan
Using software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela, which is consequently used as the input for the Spin model checker. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components.
|
guest ::
