|
|
Generating Structured Test Data
Olšák, Ondřej ; Holík, Lukáš (referee) ; Smrčka, Aleš (advisor)
The goal of the bachelor's thesis is to create a tool for generating files with structure data content. The purpose of these files is to be used as test data conforming to testing of program input space. This thesis focuses on tree-structured data. The tool integrates tools implemented previously within Testos framework for generating test data in order to satisfy user-defined coverage criterion. The tool is able to generate a set of files in JSON or XML format containing test data satisfying ECC, BCC, or PWC coverage criterion.
|
|
|
Ultrasound Simulation in Python
Černý, David ; Olšák, Ondřej (referee) ; Jaroš, Jiří (advisor)
k-Wave je MATLAB nástroj pro simulaci šíření zvukových vln. Cílem této práce je reimplementovat část nástroje k-Wave v jazyce Python se zaměřením na výpočetní výkon. Druhým cílem je formulace sady doporučení pro transformaci zdrojových kódu z jazyka MATLAB do jazyka Python, které by mohly přispět při dalším vývoji. Tato práce nejprve shrnuje klíčové funkce nástroje k-Wave, zkoumá technologie pro vysoce výkonné výpočty dostupné v jazyce Python a zdůrazňuje nejzásadnější aspekty transformace zdrojových kódů z jazyka MATLAB do jazyka Python. Druhá část práce se zabývá architekturou, testováním a měřením výkonu výsledné Python implementace. Výsledkem této práce je implementace trojrozměrné simulace šíření zvuku, která je kompatibilní s k-Wave. Nová implementace vylepšuje strukturu původního nástroje a poskytuje výkon srovnatelný s původním nástrojem, v určitých případech výkon původního balíku převyšuje.
|
|
|
Runtime Verification of Systems with MTL Properties
Olšák, Ondřej ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
|
|
|
Acceleration of Ultrasound Neurostimulation Using Mixed-Precision Arithmetic
Duchoň, Radek ; Olšák, Ondřej (referee) ; Jaroš, Jiří (advisor)
K-Wave is an open source tool for acoustic and ultrasound simulation. Current available implementations are written in C++ and Matlab. The aim of this thesis is to accelerate the existing implementation of ultrasound simulation by means of lower precision calculations on Nvidia graphics cards using the CUDA software platform. Another benefit of this work should be a reduced memory requirement, which will enable larger simulations to be performed. However, due to the use, for example, for neurostimulation of the brain, the reduced accuracy must not disturb the results as a whole too much. It is therefore important to identify suitable quantities that can be stored in lower precision. In this work, possible approaches and their effectiveness in utilizing lower precision will be analyzed. Furthermore, a solution proposal will be made, which will include identifying potential variables for reduction. This will be followed by specifying the achieved implementation and its testing. The conclusion will focus on evaluating the solution based on the results obtained from the testing.
|
|
|
Distributed Cluster Management
Bůbela, Vojtěch ; Olšák, Ondřej (referee) ; Jaroš, Jiří (advisor)
Hlavním cílem této práce je vystavět a spravovat distrubuovaný výpočetní sýstém. Dalším cílem je zajistit správné přiřazení výpočetních zdrojů clusteru a zajištění, že úloha uživatele nepřesáhne své přiřazené zdroje. Zvolený problém jsem řešil instalací a konfigurací jednoho z jichž existujících plánovačů úloh na několik výpočetních uzlů a jeden řídící uzel. Z existujících řešení jsem vybral a porovnal dva plánovače úloh, Slurm a PBS. Vytvořil jsem cluster z virtuálních počítačů a oba plánovače jsem na něj nainstaloval. Po zvážení jsem vybral plánovač Slurm. Ten jsem pak nainstaloval na 3 raspberry pi počítače a nakonfiguroval dodatečné funkce. Po zajištění základní funkcionality jsem nakonfiguroval správu přiřazovaných zdrojů na clusteru a vytvořil sadu testovacích úloh na ověřění mého řešení. Výsledkem mé práce je distribuovaný výpočetní systém s konfogirací, která splňuje požadavky zadání.
|
|
|
Ultrasound Simulation in Python
Černý, David ; Olšák, Ondřej (referee) ; Jaroš, Jiří (advisor)
k-Wave je MATLAB nástroj pro simulaci šíření zvukových vln. Cílem této práce je reimplementovat část nástroje k-Wave v jazyce Python se zaměřením na výpočetní výkon. Druhým cílem je formulace sady doporučení pro transformaci zdrojových kódu z jazyka MATLAB do jazyka Python, které by mohly přispět při dalším vývoji. Tato práce nejprve shrnuje klíčové funkce nástroje k-Wave, zkoumá technologie pro vysoce výkonné výpočty dostupné v jazyce Python a zdůrazňuje nejzásadnější aspekty transformace zdrojových kódů z jazyka MATLAB do jazyka Python. Druhá část práce se zabývá architekturou, testováním a měřením výkonu výsledné Python implementace. Výsledkem této práce je implementace trojrozměrné simulace šíření zvuku, která je kompatibilní s k-Wave. Nová implementace vylepšuje strukturu původního nástroje a poskytuje výkon srovnatelný s původním nástrojem, v určitých případech výkon původního balíku převyšuje.
|
|
|
Runtime Verification of Systems with MTL Properties
Olšák, Ondřej ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
|
|
|
Generating Structured Test Data
Olšák, Ondřej ; Holík, Lukáš (referee) ; Smrčka, Aleš (advisor)
The goal of the bachelor's thesis is to create a tool for generating files with structure data content. The purpose of these files is to be used as test data conforming to testing of program input space. This thesis focuses on tree-structured data. The tool integrates tools implemented previously within Testos framework for generating test data in order to satisfy user-defined coverage criterion. The tool is able to generate a set of files in JSON or XML format containing test data satisfying ECC, BCC, or PWC coverage criterion.
|
guest ::
