|
|
Redukce automatů používaných ve filtraci síťového provozu
Semrič, Jakub ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cieľom tejto práce je navrhnúť škálovateľné metódy pre redukciu nedeterministických konečných automatov používaných vo filtrácii paketov. Uvádzame dva prísty redukcie automatov založené na elminácii stavov. Aby sme dosiahli významnú redukciu automatu, používame techniky nezachovávajúce jazyk so zameraním na nad-aproximáciu, keďže redukcie so zachovaním pôvodného jazyka nemusia byť dostatočne účinné. Implementovali sme dané metódy a vyhodnotili presnosť redukovaných automatov na reálnych vzorkoch. Náš prístup neposkytuje žiadne formále záruky vzhľadom na nepoužité dáta, ale može byť hladko použitý na automaty akejkoľvek veľkosti, čo je hlavný problém existujúcich metód, ktoré majú vysokou časovou zložitosťou a nemôžu byť aplikované na veľké automaty.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
RPM packages are used for software installation in Fedora. Every version of software packaged in this way corresponds to a separate RPM file. Updating software therefore entails downloading a large RPM file that is actually quite similar to the RPM already installed. An alternative for software updates is provided by DeltaRPM packages, which are special patch files that store the difference between two RPM files. An update then consists of downloading a much smaller file and applying this patch to the older version of the RPM. The deltarpm project defines the format of DeltaRPM files and supplies command-line tools for creating and applying them. However, this implementation is unsuitable for use as a library. The aim of this thesis is to create a new implementation of these tools, which is backwards compatible and provides a library for C developers that solves some of the weaknesses of the current implementation.
|
|
|
Test Results Management System Complementing the tmt Tool
Dubaj, Ondrej ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
This diploma thesis deals with the area of software testing, more precisely with the topic of managing test results. The aim of this work is to find, set up and implement a system that complements the missing functionality of the TMT tool, which is going to replace the Nitrate tool in Red Hat as a test management system. The content of this work is a basic introduction to the tools Nitrate, TMT and other technologies used in Red Hat. Furthermore, the work presents the current state of the test infrastructure and collected user requirements for a new system for managing test results. Subsequently, the ReportPortal tool is introduced as a system for test results management and the missing functionality is defined. The rest of the work is devoted to setting up the system itself and implementing the missing functionality, along with implementing the infrastructure needed to import test results into ReportPortal. The work describes the method of deploying the system in use and feedback from users. The deployed system is evaluated and its further possible improvements are discussed.
|
|
|
Nástoj pro abstraktní regulární stromový model checking
Mráz, Patrik ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Formálna verifikácia sa zaoberá dokazovaním korektnosti systému podľa daných špecifikácií.Jej potrebu znásobuje stále väčšia rozšírenosť počítačov a neustály rast zložitosti aj rozsiahlosti vyvíjaných systémov. Cieľom tejto práce je implementácia nástroja formálnejverifikácie abstraktný regulárny stromový model checking (ARTMC) nad knižnicou VATA. Pre dosiahnutie tohto cieľa bolo potrebné rozšíriť knižnicu VATA o konečné stromové prevodníky,abstrakcie stromových automatov a integrovať ich spolu s nástrojom ARTMC doknižnice VATA.
|
|
|
Monitorování výkonnosti systému MES PHARIS
Ondráček, Aleš ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato diplomová práce se zabývá monitorováním výkonnosti automatizovaných procesů vývoje a výkonnostním testováním systému MES PHARIS. Hlavní náplní práce je sběr dat o úlohách prováděných na automatizačních serverech DevOps a Jenkins, zpracování těchto dat a jejich následná vizualizace. V druhé části diplomové práce je pak řešeno zpracování dat z výkonnostního testování a jejich vhodná reprezentace pomocí vizualizací. Stěžejní technologie, která je využita k řešení této problematiky, je ELK Stack.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
| |
|
|
Sběr výkonnostních parametrů systému MES PHARIS
Oháňka, Martin ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato diplomová práce se zabývá sledováním automatizovaných úloh na integračních serverech a získání dat z těchto úloh. Další rovinou této práce je výkonnostní testování a z něj získat informace o vytížení hardwaru. Díky tomu je možné provádět výkonnostní analýzy implementovaného řešení z různých výkonnostních pohledů. Výsledkem této diplomové práce je programové řešení, které je schopné získat data o úlohách z integračních serverů DevOps a Jenkins. V oblasti výkonnostního testování je vytvořeno řešení pro paralelní provádění úloh. Výstupem této práce je formátovaný výstupu předávaný formátem JSON. Data jsou následně předávána do platformy Elastic, konkrétně Logstash, kde jsou následně vizualizována pomocí Kibana. Ke sběru dat z výkonnostního testování je využita platforma Beat. Řešení bylo aplikováno na výrobní informační systém MES PHARIS společnosti UNIS.
|
|
| |
|
| |
host ::
RSS.