|
|
Symbolic Representation of Finite Automata
Chromečka, Jiří ; Vojnar, Tomáš (referee) ; Lengál, Ondřej (advisor)
In formal analysis we often encounter finite automata with a~large amount of states over large alphabets. Their explicit representation can result in a~state explosion and this problem can be solved by the use of symbolic representation that can manipulate a~whole set of states at once. The aim of this work is to extend the libVATA library to support such a~representation including algorithms for some operations on this representation. The presented text first deals with prerequisites necessary to undestand finite automata and binary decision diagrams used for their symbolic representation. Then it lists some existing libraries for work with finite automata. Next follows the core of this work, the~design of a~symbolic representation and operations on it, which are later implemented in the previously mentioned library. The test results proves that the symbolic representation is an interesting alternative to the explicit representation.
|
|
|
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Táto práca popisuje návrh a implementáciu nového riešenie pre nástroj DiffKemp na automatické dopredné prerezávanie programov. Po zdĺhavej analýze súčasného riešenia, sme sa rozhodli súčasné riešenie ponechať a rozšíriť ho o zopár vylepšení. Implementovali sme rozšírenie ktoré dovoľuje DiffKempu vykonávať analýzu nad prvkami štrukturovaných typov, pridali sme k súčasnému prerezávaciemu kritériu aj hodnotu premennej a na záver pridali podporu na analýzu parametrov modulov jadra. Po implementovaní týchto vylepšení sme vykonali experimenty ktoré potvrdili zlepšenie analýzi ktorú DiffKemp vykonával.
|
|
|
Automated Generation of Tests for GNOME GUI Applications Using AT-SPI Metadata
Krajňák, Martin ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je vývoj nástroja na automatické generovanie testov pre aplikácie s grafickým užívateľským rozhraním v~prostredí GNOME. Na generovanie testov sú použité metadáta asistenčných technológií, konrétne AT-SPI. Navrhnutý generátor testov využíva dané metadáta na vytvorenie modelu testovanej aplikácie. Model mapuje sekvencie udalostí, ktoré generátor vykoná na testovanej aplikácii počas generovania testov. Súčasťou procesu generovania je zároveň detekcia závažných chýb v testovaných aplikáciách. Výstupom procesu generovania sú automatizované testy, ktoré sú vhodné na regresné testovanie. Funkčnosť implementovaného generátora testov bola úspešne overená testovaním 5 aplikácií s otvoreným zdrojovým kódom. Počas testovania aplikácií navrhnutým nástrojom sa preukázala schopnosť detekovať nové chyby.
|
|
|
Network Monitor for Gnome
Hrozek, Jakub ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The thesis presents a new network monitoring application for the Linux operating system. It is the first graphical application with such functionality which monitors wide range of network traffic aspects and operates in graphical environment. It is integrated into the GNOME desktop environment and is also integrated into Fedora Linux distribution. The thesis discusses similar existing tools, the key part of the thesis is design, implementation and testing of the application.
|
|
|
Unified Reporting for Performance Testing
Kůrová, Martina ; Vojnar, Tomáš (referee) ; Šimková, Hana (advisor)
Moderní pokrok v oblasti technologií pro vývoj dnešních softwarových aplikací umožnil vývojářům více se soustředit na vývoj funkčnosti aplikace na úkor sledování jejího výkonu a správy zdrojů. V důsledku toho se zvýšily požadavky na nástroje pro výkonnostní testování, které by měly poskytovat vývojářům jasný a srozumitelný přehled o stavu systému z hlediska jeho výkonu a umožnit rychlou interpretaci naměřených výsledků. Tato práce zkoumá typické výkonnostní problémy dnešních aplikací a navrhuje přístupy, pomocí kterých je možné tyto anomálie automaticky rozpoznat. Pomocí statistických metod, jako je regresní a korelační analýza, je provedena analýza dat naměřených během výkonnostního testování s cílem rozpoznat ve výsledcích odchylky od normálního chování a z nich identifikovat výkonnostní problémy. Výsledkem je report o celkovém stavu systému z hlediska jeho výkonu. Implementací regresní analýzy je možné detekovat výkonnostní problémy jako je například zhoršující se reakční čas odpovědi, nízká propustnost systému či odhalit únik paměti. Navrhovaný přístup byl implementován v podobě nové komponenty v open-source nástroji pro výkonnostní testování PerfCake. Vyvinutá komponenta je schopna detekovat a reportovat potenciální výkonnostní problémy a jejich pravděpodobnost.
|
|
|
Optimize the ext4 Unlink Process to Make Recovering Deleted Files Easier
Uhliarik, Luboš ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
This thesis aims at changes of ext4 file system for optimizing unlink process and making undelete process easier. Part of the thesis descibes changes which were made in ext4 file system, including description of tool which was created as a part of this thesis for undeleting files. The thesis also includes description of tests which were used for testing modificated ext4 file system. In this thesis there are also described existing methods for undeleting deleted files, including all their advantages and disadvantages.
|
|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (referee) ; Farchi, Eitan (referee) ; Vojnar, Tomáš (advisor)
V dnešní době jsou vícevláknové programy běžné a s nimi i chyby v souběžnosti. Během posledních let bylo vytvořeno mnoho technik pro detekci takovýchto chyb, a i přesto mají vývojáři softwaru problém nalézt správné nástroje pro analýzu svých programů. Důvod je jednoduchý, fungující neznamená vždy praktický. Hodně nástrojů implementujících detekční techniky je obtížně použitelných, přizpůsobených pro konkrétní typy programů nebo synchronizace, nebo špatně škálují, aby zvládly analyzovat rozsáhlý software. Pro některé typy chyb v souběžnosti dokonce ani neexistují nástroje pro jejich detekci, i přesto že vývojáři softwaru na tyto chyby často narážejí ve svých programech. Hlavním cílem této práce je navrhnout nové techniky pro detekci chyb ve vícevláknových programech. Tyto techniky by měly být schopny analyzovat rozsáhlé programy, umožnit detekci méně studovaných typů chyb v souběžnosti, a podporovat širokou škálu programů s ohledem na to, jaké programové konstrukce používají.
|
|
|
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.
|
|
|
A Tool for Analyzing Performance of Memory Allocators in Linux
Müller, Petr ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
This diploma thesis presents a tool for dynamic memory allocator analysis, focused on their performance. The work identifies the important memory allocator performance metrics, as well as the environment and program factors influencing these metrics. Using this knowledge, a tool was designed and implemented. This tool allows to gather and analyze these metrics. The tool provides the ability to create memory allocator usage scenarios for the purpose of the allocator behavior analysis under different conditions. The tool was tested on several available memory allocators with free license.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
guest ::
