|
|
Generování strukturovaných testovacích dat
Olšák, Ondřej ; Holík, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této práce je vytvořit nástroj umožňující generovat soubory obsahující strukturovaná data za účelem testování na základě vstupních domén. Tato práce se soustředí na stromově strukturovaná data. Nástroj integruje již dříve implementované nástroje pro tvorbu testovacích dat splňujících uživatelem vybrané kritérium pokrytí vstupních domén. Vytvořený nástroj je schopen generovat sady testovacích souborů ve formátu JSON a XML s testovacími daty, které splňují kritérium pokrytí ECC, BCC nebo PWC.
|
|
|
Ultrasound Simulation in Python
Černý, David ; Olšák, Ondřej (oponent) ; Jaroš, Jiří (vedoucí práce)
k-Wave is a MATLAB toolbox for the simulation of sound wave propagation. The aim of this thesis is to re-implement a subset of k-Wave in Python while focusing on computational performance. The second goal is to develop a set of guidelines for transforming MATLAB source code to Python that could aid in further development. The thesis first summarises core features of the k-Wave toolbox, explores available technologies for high performance computing in Python, and highlights the most important aspects of transforming MATLAB source codes to Python. The second part of the thesis discusses architecture, testing and benchmarking of the Python implementation. The result of this thesis is a Python implementation of the three-dimensional sound propagation simulation compatible with k-Wave. The new implementation improves the structure of the original toolbox while providing performance comparable to the original k-Wave. In some instances, the performance of the new implementation surpasses the original implementation.
|
|
|
Verifikace za běhu systémů s vlastnostmi v MTL logice
Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem algoritmu pro ověřování splnitelnosti omezení programu zapsaných pomocí metrické temporální logiky (MTL), kdy sledování splnitelnosti těchto formulí probíhá za běhu daného programu. K ověřování těchto vlastností využívá navržený algoritmus stromové struktury, která je podobná chování alternujícího časového automatu, ze kterého je výsledný postup sledování programu odvozen. Navržený algoritmus, je schopen za běhu daného programu ověřovat jeho vlastnosti vůči definovaným MTL formulím a to bez potřeby pamatovat si stavy, ve kterých se sledovaný program nacházel. To umožňuje ověřit vlastnosti daného programu u potenciálně nekonečných běhů.
|
|
|
Akcelerace ultrazvukové neurostimulace pomocí aritmetiky se sníženou přesností.
Duchoň, Radek ; Olšák, Ondřej (oponent) ; Jaroš, Jiří (vedoucí práce)
K-Wave je nástroj pro akustickou a ultrazvukovou simulaci s otevřeným zdrojovým kódem. Aktuální dostupné implementace jsou napsány v jazycích C++ a Matlab. Cílem této diplomové práce je akcelerovat existující implementaci ultrazvukové simulace pomocí výpočtů s nižší přesností na grafických kartách Nvidia za využití softwarové platformy CUDA. Dalším přínosem této práce by měla být snížená paměťová náročnost, což umožní provádění větších simulací. Snížená přesnost však nesmí vzhledem k využití například pro neurostimulaci mozku příliš narušit výsledky jako celek. Důležité je proto identifikovat vhodné veličiny, které lze uložit v nižší přesnosti. V této práci budou analyzovány možné přístupy a jejich efektivita při využití nižší přesnosti. Dále pak bude proveden návrh řešení, jehož částí bude identifikace potenciálních veličin pro redukci. Na to bude navazovat specifikace docílené implementace a její testování. Závěr se bude věnovat zhodnocení řešení na základě dosažených výsledků z testování.
|
|
|
Distributed Cluster Management
Bůbela, Vojtěch ; Olšák, Ondřej (oponent) ; Jaroš, Jiří (vedoucí práce)
The main goal of my bachelors thesis is to build and manage a distributed computing cluster. The secondary goal is to ensure that the resource of the cluster are assigned correctly and that a job submitted by the user cannot consume more resources than it was given. I solved this problem by installing and configuring a task scheduler software on multiple compute nodes and one head node. When choosing the task scheduler I considered Slurm and PBS. I compared these two by installing and configuring them on a virtual machine cluster. After consideration i decided to go with the Slurm task scheduler. I installed it on 3 raspberry pi 3B computers using ansible and configured basic functionality. The next step was to configure correct assignment and control of resources and create set of tasks that could demonstrate that I managed to meet the goals of my thesis. The result of my thesis is a distributed computing cluster with a configuration that satisfies the main goal of my thesis. The secondary goal was also met fully.
|
|
|
Ultrasound Simulation in Python
Černý, David ; Olšák, Ondřej (oponent) ; Jaroš, Jiří (vedoucí práce)
k-Wave is a MATLAB toolbox for the simulation of sound wave propagation. The aim of this thesis is to re-implement a subset of k-Wave in Python while focusing on computational performance. The second goal is to develop a set of guidelines for transforming MATLAB source code to Python that could aid in further development. The thesis first summarises core features of the k-Wave toolbox, explores available technologies for high performance computing in Python, and highlights the most important aspects of transforming MATLAB source codes to Python. The second part of the thesis discusses architecture, testing and benchmarking of the Python implementation. The result of this thesis is a Python implementation of the three-dimensional sound propagation simulation compatible with k-Wave. The new implementation improves the structure of the original toolbox while providing performance comparable to the original k-Wave. In some instances, the performance of the new implementation surpasses the original implementation.
|
|
|
Verifikace za běhu systémů s vlastnostmi v MTL logice
Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem algoritmu pro ověřování splnitelnosti omezení programu zapsaných pomocí metrické temporální logiky (MTL), kdy sledování splnitelnosti těchto formulí probíhá za běhu daného programu. K ověřování těchto vlastností využívá navržený algoritmus stromové struktury, která je podobná chování alternujícího časového automatu, ze kterého je výsledný postup sledování programu odvozen. Navržený algoritmus, je schopen za běhu daného programu ověřovat jeho vlastnosti vůči definovaným MTL formulím a to bez potřeby pamatovat si stavy, ve kterých se sledovaný program nacházel. To umožňuje ověřit vlastnosti daného programu u potenciálně nekonečných běhů.
|
|
|
Generování strukturovaných testovacích dat
Olšák, Ondřej ; Holík, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této práce je vytvořit nástroj umožňující generovat soubory obsahující strukturovaná data za účelem testování na základě vstupních domén. Tato práce se soustředí na stromově strukturovaná data. Nástroj integruje již dříve implementované nástroje pro tvorbu testovacích dat splňujících uživatelem vybrané kritérium pokrytí vstupních domén. Vytvořený nástroj je schopen generovat sady testovacích souborů ve formátu JSON a XML s testovacími daty, které splňují kritérium pokrytí ECC, BCC nebo PWC.
|
host ::
RSS.