|
|
A Tool for Generating Test Paths Based on a Given Criterion
Bíl, Jan ; Rogalewicz, Adam (referee) ; Smrčka, Aleš (advisor)
The automatic generation of test inputs according to a specified coverage criterion has the potential to significantly reduce costs in the development of critical applications. This work focuses on designing and implementing a tool that systematically generates paths in the control flow graph generated from function of such application, that meet the specified coverage criterion targets. These paths are then transformed into the corresponding SMT (Satisfiability Modulo Theories) format, and their feasibility is verified using the Z3 SMT solver. For paths that are feasible, a set of input valuations for which the formula holds is simultaneously generated. This collection of valuations formes a set of test inputs that effectively meet the desired coverage criterion. Final test inputs are tested function parameters and state of global parameters.
|
|
|
Length Constraints in String Solving
Hranička, Jan ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Řešení řetězcových omezení je v dnešní době základním kamenem formální verifikace s širokým vědeckým i obchodním uplatněním. Přínosem této práce je návrh nové rozhodovací procedury s cílem rozšířit jeden z předních string solverů: Z3-Noodler. Tato rozhodovací procedura je založena na symbolickém zarovnání řetězcových proměnných v rovnicích pomocí generování omezení na jejich délky. Experimenty na standartních benchmarcích ukázaly, že integrace této procedury s nástrojem Z3-Noodler vede ke snížení timeoutů o 32 a na určitých testech snižuje celkovou dobu běhu nástroje více než padesátkrát. Díky těmto přínosům je možné očekávat přidání této procedury do zmíněného nástroje.
|
|
|
Test Data Generator for Databases of Financial Technology
Moresová, Eva ; Vašíček, Ondřej (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with the creation of a test-data generator for databases of applications in the field of financial technology. The solution was implemented as an extension and modification of the functionality of existing dbgenx tool, which is a part of the Testos platform. The created tool enables data generation with regard to its structural and semantic dependencies, definition of custom external modules for data generation and provides an efficient way to define specification of the generated data.
|
|
| |
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.
|
|
|
Development of Combine Tool
Nováček, Pavel ; Janoušek, Vladimír (referee) ; Smrčka, Aleš (advisor)
This thesis deals with the reimplementation of the web tool Combine, which generates combinatorial test sets satisfying user-specified parameters and constraints using the IPOG algorithm. The thesis is a part of Testos platform, which aims at software testing automation. The goal of this thesis is to analyze the current state of the tool, identify its errors and deficiencies, discuss suitable extensions to its functionality, and based on these findings, create a new design and implementation of the Combine tool. The new solution preserves all the functionality of the previous tool and at the same time expands it on all levels of the architecture. The tool is not only more manageable thanks to a more user-friendly web interface but also offers new possibilities for test set generation. More suitable technologies have been chosen for its implementation, making the tool portable and significantly faster in generating test sets compared to the previous implementation, capable of competing with existing solutions for combinatorial test set generation.
|
|
|
Test Data Generator for Databases of Financial Technology
Moresová, Eva ; Vašíček, Ondřej (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with the creation of a test-data generator for databases of applications in the field of financial technology. The solution was implemented as an extension and modification of the functionality of existing dbgenx tool, which is a part of the Testos platform. The created tool enables data generation with regard to its structural and semantic dependencies, definition of custom external modules for data generation and provides an efficient way to define specification of the generated data.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.
|
|
| |
guest ::
