|
|
Reductions of Automata Used in Network Traffic Filtering
Semrič, Jakub ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
The aim of this work is to propose scalable methods for reducing non-deterministic finite automata used in network traffic filtering. We introduce two approaches of NFAs reduction based on states elimination. To achieve a substantial reduction of automata, we use language non-preserving techniques with a primary focus on language over-approximation, since language preserving methods may not provide sufficient reduction. We implemented the methods and evaluated the accuracy of the reduced automata on real traffic. Our approach does not provide any formal guarantee wrt unseen input traffic, but on the other hand, it can be smoothly used on automata of any size, which is a significant problem for existing methods that have very high time complexity and cannot be applied on really large automata.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Na platformě Fedora se používají balíčky RPM pro instalaci softwaru. Každá verze takto distribuovaného softwaru odpovídá samostatnému souboru RPM. Aktualizace softwaru pak odpovídá stáhnutí velkého souboru RPM, který je ve skutečnosti velmi podobný již nainstalovnému balíčku. Balíčky DeltaRPM poskytují alternativu pro aktualizaci softwaru. Jedná se o speciální patch soubory, které uchovávají rozdíl mezi dvěma soubory RPM. Aktualizace pak spočívá ve stáhnutí daleko menšího souboru a aplikaci tohoto patche na starší verzi příslušného RPM. Projekt deltarpm definuje formát souborů DeltaRPM a nabízí nástroje pro příkazovou řádku, které realizují jejich vytváření a aplikaci. Tato implementace je však nevhodná pro použití jako knihovna. Cíl této práce je vytvořit novou implementaci nástrojů pro vytváření a aplikaci souborů DeltaRPM, která je zpětně kompatibilní a poskytuje knihovnu pro vývojáře v jazyce C, která vyřeší některé slabiny současné implementace.
|
|
|
Test Results Management System Complementing the tmt Tool
Dubaj, Ondrej ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
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.
|
|
|
Tool for Abstract Regular Tree Model Checking
Mráz, Patrik ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification deals with proving the correctness of the system according to the given specifications. Its need is driven by an increasing number of computers and a increase in the complexity of the systems being developed. The aim of this work is to implement the formal verification tool abstract regular tree model checking (ARTMC) over the VATA library. To achieve this goal, it was necessary to extend the VATA library on the finite tree transducers, abstractions of tree automata and integrate them together with the ARTMC into the VATA library.
|
|
|
Performance Monitoring of MES PHARIS
Ondráček, Aleš ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This diploma thesis deals with the performance monitoring of automated development processes and performance testing of the MES PHARIS system. The main scope of thesis is the collection of data on tasks performed on automation servers DevOps and Jenkins, processing of this data and their subsequent visualization. The second part of the diploma thesis deals with the processing of data from performance testing and their appropriate representation using visualization. The core technology that is used is ELK Stack.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Detection of characteristic facial features in tele-X-ray image
Hruška, Martin ; Přinosil, Jiří (referee) ; Mišurec, Jiří (advisor)
Description cephalometric images and the characteristic points on the skull for cephalometric analysis. Theoretical analysis of digital image editing and image before the actual detection. The range of possible methods for determining the characteristic points on the face. Experimental verification of edge detectors, Hu moments with neural networks and Haar wavelets with Viola-Jones detector.
|
|
|
Performance Data Collection of MES PHARIS
Oháňka, Martin ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This master's thesis deals with monitoring of automated tasks on integration servers and obtaining data from these tasks. Another area of this work is performance testing and to obtain information about hardware utilization from it. Thanks to this, it is possible to perform performance analysis of the implemented solution from different performance perspectives. The result of this master's thesis is a software solution that can obtain data about tasks from DevOps and Jenkins integration servers. In the area of performance testing, there is created a solution for parallel execution of tasks. The output of this work an output passed in JSON format. The data is then transferred to the Elastic platform, specifically Logstash, where it is subsequently visualized using Kibana. The Beat platform is used to collect data from performance testing. The solution was applied to the production information system MES PHARIS of the UNIS company.
|
|
| |
|
| |
guest ::
RSS feed.