|
|
Program Instrumentation Enabling Coverage Measurement in SW Testing
Kapoun, Petr ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This work deals with the design and creation of an instrumentation tool for measuring coverage in software testing. During compilation, the tool obtains a representation of selected parts of the program in the form of a control flow graph and instruments the given parts of the program by inserting function callbacks. Using the data generated when calling the function callbacks of the instrumented program, the tool evaluates the measurement of the coverage criteria. Supported coverage criteria include line coverage and selected control flow and data flow coverage criteria.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
Instrumentation of C/C++ Programs during Compilation
Mušková, Kateřina ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This thesis presents design and implementation of the TforcTool offering compile-time instrumentation of memory access and functions. The tool is built on an existing static instrumenting tool Tforc, which was extended in order to provide greater usability and functionality. The advantage of this solution compared to another compile-time tools is that there is no need to change current compile structure of project.
|
|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Mnoho aplikací přijímá, odesílá a zpracovává data v textové podobě. Správné a bezpečné zpracování těchto dat je typicky zajištěno tzv. ošetřením řetězců (string sanitization). Pomocí metod formální verifikace je možné analyzovat takovéto operace s řetězci a prověřit, zda jsou správně navržené či implementované. Naším cílem je vytvořit obecný nástroj pro analýzu systémů jejichž konfigurace lze kódovat pomocí slov z vhodné abecedy, a také jeho specializaci pro analýzu programů pracujících s řetězci. Nejprve jsou popsaný konečné automaty a převodníky a poté různé třídy a podtřídy symbolických převodníků, zejména pak jejich omezení. Na základě těchto informací je pak pro použití v analýze programů navržen nový typ symbolických převodníků. Dále je popsán regulární model checking, speciálně pak jeho variantu založenou na abstrakci automatů, tzv. ARMC, u kterého je známo že dokáže velmi úspěšně překonat problém stavové exploze u automatů a umožňuje nám tzv. dosáhnout pevného bodu v analýze. Poté je navržena vlastní analýza programů psaných v imperativním paradigmatu, a to zejména programů manipulujících s řetězci, založená na principech ARMC. Následuje popis vlastní implementace nástroje s důrazem na jeho praktické vlastnosti. Rovněž jsou popsaný důležité části knihovny AutomataDotNet, na které nástroj staví. Práci je uzavřena diskuzí experimentů s nástrojem provedených na příkladech z knihovny LibStranger.
|
|
|
Search of Control Strategies Using UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (referee) ; Strnadel, Josef (advisor)
This thesis deals with finding control strategies for pre-selected problems from various areas using tool Uppaal Stratego. Four areas were selected, namely chess, a sliding puzzle, the tower of Hanoi, and a kinematic problem involving a package, a car, and an airplane. For the selected areas and problems, a set of models was designed and implemented. For the tower of Hanoi and the sliding field, it was possible to successfully evaluate relevant strategies, raising the probabilities of success to more than 90 %. For other models, a problem was found in the size of the state space and the strategies could not be evaluated because the maximum memory capacity that the tool uses was not sufficient. For the kinematic problem, after limiting and simplifying the model, the strategies were successfully evaluated, but for chess, this was not possible even after significant simplification.
|
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (referee) ; Řehák, Vojtěch (referee) ; Vojnar, Tomáš (advisor)
Předmětem dizertační práce je návrh nových technik pro verifikaci hardwaru, které jsou optimalizovány pro použití v procesu souběžného vývoje hardwaru a softwaru. V rámci tohoto typu vývoje je hardware spolu se software vyvíjen paralelně s cílem urychlit vývoj nových systémů. Současné nástroje pro tvorbu mikroprocesorů stavějící na tomto stylu vývoje obvykle umožňují vývojářům ověřit jejich návrh využitím různých simulačních technik a/nebo za pomoci tzv. funkční verifikace. Společnou nevýhodou těchto přístupů je, že se zaměřují pouze na hledání chyb. Výsledný produkt tedy může stále obsahovat nenalezené netriviální defekty. Z tohoto důvodu se v posledních letech stává stále více žádané nasazení formálních metod. Na rozdíl od výše uvedených přístupů založených na hledání chyb, se formální verifikace zaměřuje na dodání rigorózního důkazu, že daný systém skutečně splňuje požadované vlastnosti. I když bylo v uplynulých letech v této oblasti dosaženo značného pokroku, tak aktuální formální přístupy nemají zdaleka schopnost plně automaticky prověřit všechny relevantní vlastnosti verifikovaného návrhu bez výrazného a často nákladného zapojení lidí v rámci verifikačního procesu. Tato práce se snaží řešit problém s automatizací verifikačního procesu jejím zaměřením na verifikační techniky, ve kterých je záměrně kladen menší důraz na jejich přesnost a obecnost, za cenu dosažení plné automatizace (např. vyloučením potřeby ručně vytvářet modely prostředí). Dále se práce také zaměřuje na efektivitu navrhovaných technik a jejich schopnost poskytovat nepřetržitou zpětnou vazbu o verifikačním procesu (např. v podobě podání informace o aktuálním stavu pokrytí). Zvláštní pozornost je pak věnována vývoji formálních metod ověřujících ekvivalenci návrhů mikroprocesorů na různých úrovních abstrakce. Tyto návrhy se mohou lišit ve způsobu, jakým jsou vnitřně zpracovány programové instrukce, nicméně z vnějšího pohledu (daného např. obsahem registrů viditelných z pozice programátora) musí být jejich chování při provádění stejného vstupního programu shodné. Kromě těchto témat se práce také zabývá problematikou návrhu metod pro verifikaci správnosti mechanismů zabraňujících výskytu datových a řídících hazardů v rámci linky zřetězeného zpracování instrukcí. Veškeré metody popsané v této práci byly implementovány ve formě několika nástrojů. Aplikací těchto nástrojů pro verifikaci návrhů netriviálních procesorů bylo dosaženo slibných experimentálních výsledků.
|
|
|
Human Interface to Automata Libraries of MONA Tool
Pyšný, Radek ; Šimáček, Jiří (referee) ; Rogalewicz, Adam (advisor)
Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.
|
|
|
Efficient Algorithms for Büchi Automata
Laščák, Tomáš ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
The main goal of this work is to extend the existing library VATA with a module for working with Büchi automata, which are finite state automata over infinite words. These automata are used in many areas of computer science, among others in formal verifications, namely in LTL model checking. LTL model checking is typically carried out using the operation of testing language inclusion between two Büchi automata. Because testing language inclusion can be computationally very demanding, several optimized algorithms have been created for testing language inclusion such as the Ramsey-based approach. This work is focused on the mentioned approach, the implementation of which is added to the newly created extension of the VATA library. Apart from that, the new extension adds additional useful operations over Büchi automata such as union, intersection or a reduction in the number of states.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
guest ::
