|
|
Distributed Behavior Protocol Checker
Poch, Tomáš ; Adámek, Jiří (referee) ; Kofroň, Jan (advisor)
Growth of the computability power in the last years enabled practical use of model checking of software systems. However the state space explosion is still a burning problem that limits usage of this technique to the relatively small tasks. One of the approaches that significantly decrease state space of the task is Behavior Protocol [1]. Behavior protocol is regular language that describes behavior of software component so that component implementation details are hidden during checking of whole application - what is reduced to the checking whether behavior protocols of used components are compliant. However even checking of behavior protocols compliance faces the exponential growth of number of states. Distributed state space traversing together with 'on the fly' state space generation [2] can be used to improve both time and space requirements.
|
|
|
Extending Java PathFinder with Behavior Protocols
Plšek, Aleš ; Kofroň, Jan (referee) ; Adámek, Jiří (advisor)
The Component-based programming is an aproach to efficient development of software applications, where Behavior protocol is a formalism used for behavior specification of components. To further ease the development of a component application, System Correctness analysis is employed to discover errors at the designe time. However, without verifying that a component implementation complies with its behavior protocol, the analysis of the system could be based on unsatisfied property. This thesis addresses the problem of verification that a component implementation adheres to its behavior protocol. By employing Java PathFinder Model Checker it offers an ambitious solution which is successfully addressing one of the issues of the software component development.
|
|
|
Merging of Different Text File Versions
Trochtová, Lenka ; Kofroň, Jan (referee) ; Ježek, Pavel (advisor)
The goal of this thesis is to create a program (Merge) for comparing and merging two or three versions of text files and directories. The thesis describes the program from both user's and programmer's points of view. The text includes introduction into the background of file comparing and merging, comparison of the Merge program with another existing merging tools, a brief description of the main functions of the Merge program and also description of design and implementation of the program including the algorithms of text and directory comparison.
|
|
|
Combining temporal logic and behavior protocols
Mandys, Petr ; Kofroň, Jan (referee) ; Adámek, Jiří (advisor)
In this thesis we consider one of the weaknesses of temporal logic - the fact that the temporal formulas specifying complex properties are hard to read. We introduce new temporal logic "BP-CTL", that originate from Computational Tree Logic (CTL) extended with operators partly taken from Behavior Protocols (BP) and partly newly defined. Text of the thesis is divided into several parts. First we introduce reader to the context of the issue. Next we describe new operators and show their usage on small examples. Then we formally define the resulting language (BP-CTL). In the next part we demonstrate the usability of BP-CTL and introduce the tool - called bpctl - for checking properties written in BP-CTL. Finally we evaluate and conclude our work. The text is extended with appendixes including detailed description of used formalisms, mapping tables of patterns collected in Property Specification Patterns project for BP-CTL and bpctl user manual.
|
|
|
Post-quantum alternative to secure sockets
Behún, Marek ; Kratochvíl, Miroslav (advisor) ; Kofroň, Jan (referee)
The goal of this thesis is to implement a software library that provides a wrapping of real-time socket- like communication into an cryptographic protocol with purpose similar to SSL or TLS, that is secure against an adversary in possession of a quantum computer. Resulting software utilizes the Supersingular Isogeny Diffie Hellman (SIDH) key-exchange algorithm for achieving this level of security, and is simple, portable and independent on system-specific primitives. The thesis gives a concise introduction to the theory on which SIDH is built, targeting the audience of undergraduate students of Computer Science. Powered by TCPDF (www.tcpdf.org)
|
|
|
Code Assertions Verification Using Backward Symbolic Execution
Husák, Robert ; Kofroň, Jan (advisor) ; Parízek, Pavel (referee)
In order to prevent, detect and fix errors in software, various tools for programmers are available, while some of them are able to reason about the behaviour of the program. In the case of C# programming language, the main representatives are Microsoft FxCop, Code Contracts and Pex. Those tools can, indeed, help to build a highly reliable software. However, when a company wants to include them in the software development process, there is a significant overhead involved. Therefore, we created a "light- weight" assertion verification tool called AskTheCode that can help the user to focus on a particular problem at a time that needs to be solved. Because of its goal-driven approach, we decided to implement it using backward symbolic execution. Although it can currently handle only basic C# statements and data types, the evaluation against the existing tools shows that it has the potential to eventually provide significant added value to the user once developed further. Powered by TCPDF (www.tcpdf.org)
|
|
|
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 ::
