|
|
Model-Based Testing of JBoss Drools
Široký, Petr ; Holík, Lukáš (referee) ; Letko, Zdeněk (advisor)
Model-based testing (MBT) is using a model of expected behavior of the system to automatically generate a set of tests. It aims at reducing the testing cost when compared to the traditional testing techniques. This work focuses on testing a real-world software system using the selected MBT tool OSMO. The tested system is responsible for compiling business rules and it is one of the main components of the Drools platform, developed by Red Hat. The work describes the introduction of MBT considering the good reception from the community of developers, then the creation of compiler input models and evaluation of the newly created test suite. The usage of the MBT resulted in detection of five reported and three potential issues in the tested code. Using the Drools compiler example, the work summarizes the main strengths and also weaknesses of practical use of MBT techniques.
|
|
|
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.
|
|
|
Merging Tasks with Non-Interfering Requests for the System Baker
Kovařík, Michal ; Fiedor, Jan (referee) ; Holík, Lukáš (advisor)
The goal of this thesis is to design a format for entering parameters and requirements of individual tasks intended for the Beaker system and to design a program that merges tasks defined upon input based on elimination of possible collision requirements into collection of tasks that can be run together. The output format should be acceptable by the Beaker system. The thesis describes installation of the operating system on which collision requirements are defined. The thesis describes how to specify and run tasks in the Beaker system. The results of the program testing are shown in the thesis' conclusion.
|
|
|
Practical Efficiency of Containers
Halámka, Jan ; Letko, Zdeněk (referee) ; Holík, Lukáš (advisor)
This thesis is about theorethical and practical comparrison of following data containers: vector, deque, list, hash table, avl-tree, rb-tree, splay-tree, sg-tree, treap, B-tree, binomial heap, fibonacci heap, rope and skiplist while implementing sets. Asymptotic, amortized and average-case complexity for each of those structures are noted, as well as details about their implementation and description of how are they stored in computer memory. There was also created a set of tests for comparrison purposes, its results are also part of this paper.
|
|
|
A Library for Binary Decision Diagrams
Janků, Petr ; Hrubý, Martin (referee) ; Holík, Lukáš (advisor)
Efficient manipulation of Boolean functions is an important component of many computer-aided design task. As a data structure for representing and manipulating Boolean functions, Binary Decision Diagrams are commonly used. These diagrams are commonly used in many fields such as model checking, system verification, circuit design, etc. In this thesis we describe these diagrams and there are present their modifications. Furthermore, this paper present and describes techniques for effective handling and representation of binary decision diagrams. This thesis describes the design and implementation of library that will work with these diagrams. It is further discussed how the developed library can be used within the library VATA for manipulating tree automata. Finally, the library was compared with well known and heavily optimized library CUDD, which is public and with library CacBDD. The experimental results showed that the performance of the proposed library is quite close to that of CUDD a CacBDD (has comparable and mostly even slightly better performance).
|
|
|
Test Optimization by Search-Based Algorithms
Starigazda, Michal ; Holík, Lukáš (referee) ; Letko, Zdeněk (advisor)
Testing of multi-threaded programs is a demanding work due to the many possible thread interleavings one should examine. The noise injection technique helps to increase the number of tested thread interleavings by noise injection to suitable program locations. This work optimizes meta-heuristics search techniques in the testing of concurrent programs by utilizing deterministic heuristic in the application of genetic algorithms in a space of legal program locations suitable for the noise injection. In this work, several novel deterministic noise injection heuristics without dependency on the random number generator are proposed in contrary to the most of currently used heuristic. The elimination of the randomness should make the search process more informed and provide better, more optimal, solutions thanks to increased stability in the results provided by novel heuristics. Finally, a benchmark of programs, used for the evaluation of novel noise injection heuristics is presented.
|
|
|
Coverability for Parallel Programs
Turoňová, Lenka ; Vojnar, Tomáš (referee) ; Holík, Lukáš (advisor)
This work is focusing on automatic verification of systems with parallel running processes. We discuss the existing methods and certain possibilities of optimizing them. Existing techniques are essentially based on finding an inductive invariant (for instance using a variant of counterexample-guided abstract refinement (CEGAR)). The effectiveness of these methods depends on the size of the invariant. In this thesis, we explored the possibility of improving the methods by focusing on finding invariants of minimal size. We implemented a tool that facilitates exploring the space of invariants of the system under scrutiny. Our experimental results show that many practical existing systems indeed have invariants that are much smaller than what can be found by the existing methods. The conjectures and the results of the work will serve as a basis of future research of an efficient method for finding small invariants of parallel systems.
|
|
|
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.
|
|
|
The Study of Optimization of Production Process
Holík, Lukáš ; tesař, Rostislav (referee) ; Jurová, Marie (advisor)
The master thesis: „ The Study of Optimization of Production Process“ focouses on optimization of material flow to manufacturing department. First of all there will be shown theoretical approach corresponding with the thesis area and we will introduce production system and portfolio of products. Subsequently a real project will be analyzed and author will describe deficiencies in this project and system. Thanks to theoretical approach there will be found a different solution how to define new system without deficiencies. In the end the author will make a conclusion of newly found solution
|
|
|
Business Plan
Holík, Lukáš ; Novák, Zdeněk (referee) ; Rompotl, Jaroslav (advisor)
The goal of this dissertation is to create a business plan for mr. David Mokrý - owner of café Blue Queen in Boskovice. In a short time he would like to make his business bigger and found another café - pub (Black King).The needed data for creating a project of new successful restaurant, which should become the most popular in selected location, I'm going to get by many market analyses, respective by analyses of internal and external neighborhood.
|
guest ::
RSS feed.