|
|
A Control System for Applications Testing in Linux
Beneš, Eduard ; Vojnar, Tomáš (referee) ; Smrčka, Aleš (advisor)
This thesis discusses the area of a control system for application testing in Linux. There is a need for testing software and its quality using automated software tools. Huge number of testing tools is available, Red Hat Test System (RHTS) being one of them. Dierent approaches to classi cation and evaluation of a testing tools are presented. Selected software testing tools were evaluated and compared with RHTS. The thesis then presents a design of a system for non-interactive application testing in Linux with support for RHTS tests and with focus on future enhancements. Implemented system is nally tested using proposed set of tests and several usage examples are described.
|
|
|
Program Similarity Recognition Based on Behaviour Analysis
Otočka, Dávid ; Vojnar, Tomáš (referee) ; Peringer, Petr (advisor)
The goal of this master thesis was to design an algorithm that will be able to measure the difference between two programs based on their behavioral description. For the algorithm needs, the Levenshtein distance method between two strings and NCD method, were used. Both methods have their implementation approach and test result described. This term also discusses various methods of program analysis in virtual machine environment, as well as explanation of some basic concepts regarding malware analysis.
|
|
|
Static Value Analysis over C Programs
Ďuričeková, Daniela ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
Value-range analysis is a static analysis technique based on arguing about the values that a variable may take on a given program point. It can be used to prove absence of run-time errors such as out-of-bound array accesses. Since value-range analysis collects information on each program point, data-flow analysis can be used in association with it. The main goal of this work is designing and implementing such a value-range analysis tool. The work begins with an introduction into the topic, an explanation of data-flow and value-range analyses and a description of abstract interpretation, which provides the formal basis of the analyser. The core of this work is the design, implementation, testing and evaluation of the analyser. In the conclusion, our personal experience obtained in the area of the thesis is mentioned, along with a discussion of a possible future development of the designed tool.
|
|
|
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.
|
|
|
Shared Board
Řezník, Jaroslav ; Mazal, Zdeněk (referee) ; Vojnar, Tomáš (advisor)
The aim of the "Shared Board" project is to design and implement an application that will allow a real-time collaboration on workgroup projects in a network environment. The communication can be accomplished using Instant Messaging or multimedia whiteboard with a possibility of drawing, attaching interactive objects and combined with voice and video communication. The term project part solves utilization of interactive whiteboards, design of communication protocol and grafical user interface. Implementation is solved as masters thesis part.
|
|
|
Microkernels of Operating Systems
Beneš, Eduard ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
This thesis discusses the area of microkernel based operating systems. The first part is focused on the familiarization with the issue of the operating system kernel. This part contains the basic characteristics and mechanisms of the second generation microkernels represented by the microkernel L4, on which there is major focus in other parts of the thesis. Subsequently, there are described two different ports of the operating system Linux on top of L4 microkernel and those are L4Linux and Wombat. In the second part of the thesis, the method of the installation of the given ports is depicted and the main problems the author had to face. The third and forth part are focused on the issue of testing the performance of the installed systems. The methodology of chosen experiments is described and the meaning of the individual tests explained. The results, as well as their evaluation are stated in the forth part. If suitable, the gained results are compared with each other, or with the results gained from the Internet. In the last part, a short discussion is conducted based on the gained knowledge on the issue of the possibilities of microkernel application.
|
|
|
Static Analysis of C Programs in Sparse and Similar Tools
Nagy, Martin ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
Software verification is steadily becoming important for software developers and companies to ensure software quality. However, the problem of writing a good static code analysis tool often stems from the lack of a good compiler front-end. To solve this problem, we try to analyse and document an existing tool called Sparse to empower software verification researchers with a ready, stable solution for their projects. Additionally, we also talk about Mygcc and it's new approach to integrate with existing compilers.
|
|
|
Snapshot and Rollback Support for Configuration Files in Fedora
Ježek, Michal ; Vojnar, Tomáš (referee) ; Smrčka, Aleš (advisor)
The purpose of this thesis is to design and implement tools for support of a snapshot and a rollback for configuration files on the GNU/Linux distribution. The set of the tools enables an automatic/periodical saving of the configuration files into the selected placement. The creation of backups reacts to file events by watching the changes with kernel subsystem inotify. Tools are enabling to return to the selected backup. The way of the backup actualization is configurable. This tool permits the data comparison from selected backups, to show the differences in configurations and eventually to manage a merge among actual and selected backup. Tools also allows a comparison of a configurations of one client or configurations among clients, and to display the mutual differences, eventually to manage their merge.
|
|
|
Automated Test Documentation Generator for BeakerLib Tests
Kulda, Jiří ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The aim of this work in cooperation with Red Hat Czech company is to design, implement and verify documentation generator for test written using BeakerLib library, which effectively creates documentation from BeakerLib tests without any documentation markup. In the first step generator parses data from every BeakerLib command in the test. Subsequently data are transformed as a natural language information. At the end generator transforms this information into documentation template. In this case an argparse method was used to find possible data from BeakerLib commands. In contrast to existing documentation generators this generator brings a new way of documentary creation from tests without any documentation markup. Thanks to this point of view we can generate documentation, which is created on base of automated understanding of test source code. Through documentation generator development time the generator was tested on three BeakerLib tests. In the end the documentation generator was tested on ten BeakerLib tests which were randomly selected.
|
|
|
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.
|
guest ::
