Search

Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje., Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.

Cílem této práce je vytvořit komunikační sběrnici pro platformu Testos, což umožní nástrojům platformy spolu komunikovat a využívat navzájem svoje služby. V textu jsou prozkoum8na současná řešení a protokoly založené na modelu Publish-Subscribe. Dále také práce specifikuje požadavky na komunikační sběrnici vyhovující potřebám platformy Testos a také navrhuje řešení pro splnění daných požadavků. V rámci výzkumu byly prozkoumány tři řešení - MQTT, DDS a AMQP. Průzkum každého řešení byl zaměřen na způsob komunikace a hlavní funkční prvky. Jako startovací bod implementace sběrnice byl vybrán protokol MQTT. Tato práce také specifikuje jak tento protokol rozšířit, aby byly splněny požadavky na sběrnici. Mezi stěžejní rozšíření navrhnuté v rámci této práce patří management životního cyklu požadavků rozšiřující způsob doručování zpráv a mechanismus zasílání požadavků standardu MQTT. Protokol byl také rozšířen o možnost shlukování zpráv do BULK paketu za účelem snížení množství potřebných síťových zdrojů. Výsledkem je Testos Bus, který je postavený na upraveném a rozšířeném protokolu MQTT, který zahrunuje implementaci brokeru a klientských knihoven pro Python a C++. Testos Bus naplňuje všechny povinné požadavky platformy, což ověřují automatické testy., This goal of this thesis is to create a communication bus for the Testos platform, which enables the tools to communicate and utilize each other's services. The thesis consists of a research of current Publish-Subscribe protocols and solutions. It also outlines the requirements for a communication bus that fits the Testos platform's needs and proposes solutions that satisfy them. As a part of the research, there were 3 message-oriented software solutions explored - MQTT, DDS and AMQP. The examination of each solution was focused on the communication model and main features. The MQTT protocol was chosen as the starting point of the bus implementation. The thesis also specifies how to extend the protocol in order to satisfy the requirements. Main MQTT extensions proposed by this project include an introduction of a management of request life cycle on top of the MQTT message delivery and the request/response mechanism. The protocol was also expanded by ability to pack messages into a BULK packet to decrease the needed network resources. The result is a Testos Bus, which is based on a modified and expanded version of MQTT, that includes a broker implementation as well as implementation of client libraries for Python and C++. Testos Bus satisfies all mandatory requirements, which is verified by automated tests.

Cílem této práce je vytvořit komunikační sběrnici pro platformu Testos, což umožní nástrojům platformy spolu komunikovat a využívat navzájem svoje služby. V textu jsou prozkoum8na současná řešení a protokoly založené na modelu Publish-Subscribe. Dále také práce specifikuje požadavky na komunikační sběrnici vyhovující potřebám platformy Testos a také navrhuje řešení pro splnění daných požadavků. V rámci výzkumu byly prozkoumány tři řešení - MQTT, DDS a AMQP. Průzkum každého řešení byl zaměřen na způsob komunikace a hlavní funkční prvky. Jako startovací bod implementace sběrnice byl vybrán protokol MQTT. Tato práce také specifikuje jak tento protokol rozšířit, aby byly splněny požadavky na sběrnici. Mezi stěžejní rozšíření navrhnuté v rámci této práce patří management životního cyklu požadavků rozšiřující způsob doručování zpráv a mechanismus zasílání požadavků standardu MQTT. Protokol byl také rozšířen o možnost shlukování zpráv do BULK paketu za účelem snížení množství potřebných síťových zdrojů. Výsledkem je Testos Bus, který je postavený na upraveném a rozšířeném protokolu MQTT, který zahrunuje implementaci brokeru a klientských knihoven pro Python a C++. Testos Bus naplňuje všechny povinné požadavky platformy, což ověřují automatické testy., This goal of this thesis is to create a communication bus for the Testos platform, which enables the tools to communicate and utilize each other's services. The thesis consists of a research of current Publish-Subscribe protocols and solutions. It also outlines the requirements for a communication bus that fits the Testos platform's needs and proposes solutions that satisfy them. As a part of the research, there were 3 message-oriented software solutions explored - MQTT, DDS and AMQP. The examination of each solution was focused on the communication model and main features. The MQTT protocol was chosen as the starting point of the bus implementation. The thesis also specifies how to extend the protocol in order to satisfy the requirements. Main MQTT extensions proposed by this project include an introduction of a management of request life cycle on top of the MQTT message delivery and the request/response mechanism. The protocol was also expanded by ability to pack messages into a BULK packet to decrease the needed network resources. The result is a Testos Bus, which is based on a modified and expanded version of MQTT, that includes a broker implementation as well as implementation of client libraries for Python and C++. Testos Bus satisfies all mandatory requirements, which is verified by automated tests.

Tato práce se zaměřuje na vytvoření webové komponenty k vykreslení grafů ze strukturovanýho datovýho formátu (dále jen schéma) a vytvoření uživatelského rozhraní pro editaci schématu pro Ansible Automation Analytics. Práce zkoumá aktuální implementaci Ansible Automation Analytics a odpovídající API. Dále zkoumá vhodné knihovny pro vykreslování grafů a popisuje základy použitých technologií. Praktická část popisuje požadavky na komponentu a popisuje vývoj a implementaci pluginu. Dále práce popisuje proces testování a~plány budoucího vývoje pluginu., This thesis focuses on creating a web component to render charts from a structured data format (schema for short), and creating an user facing interface for editing and creating the schema for the Ansible Automation Analytics. The thesis explores the current implementation of the Ansible Automation Analytics and the corresponding API, researches similar charting libraries and describes the fundamentals of used technologies. The practical part describes the requirements for the component and describes the development and the implementation of the plugin. Furthermore, the thesis describes the process of testing and the future development plans of the plugin.

Práce si klade za úkol poskytnout čtenáři popis statické analýzy prováděné prostřednictvím nástroje FindBugs nad aplikačním serverem JBoss od společnosti Red Hat. Na základě analýzy vybraných chyb byly vytvořeny vzory pro jejich detekci, které byly následně naimplementovány jako zásuvné moduly statického analyzátoru FindBugs (tzv. detektory). Vytvořené detektory byly otestovány na vývojové verzi JBoss aplikačního serveru a výsledky jsou publikovány v závěru práce., First, a few bugs from a list of common bug were chosen and patterns describing these bugs were inferred. Then, detectors searching for such patterns were implemented as plug-ins to FindBugs static analyzer. Finally, detectors were used to detect bugs in development version of JBoss AS. Results are presented at the end of this paper.

Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje., Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.

Cieľom práce je minimalizovať čas strávený modelovaním softvérovej architektúry a poskyt- núť praktický nástroj na vytváranie, zoraďovanie a vizualizáciu systémových modelov. Súčasné prístupy k modelovaniu zaberajú príliš veľa času, pričom vytvorenie a úpravy modelu často stoja viac času ako ich implementácia. Práca sa zameriava predovšetkým na efektívne zobrazenie zložitých modelov, nájdenie najlepšieho modelovacieho jazyka na vykonávanie tejto úlohy a vytvorenie agilného editora., The thesis aims to minimize time spent on modeling software architecture and provide a practical tool to create, order, and visualize system models. The current modeling ap- proaches consume too much time, often creating and editing the model costs more time than implementing such a system. The work focuses primarily on representing complex models efficiently, finding the best modeling language to do this task, and developing an agile editor.

Cieľom tejto práce je navrhnúť a naprogramovať testovací modul na testovanie užívateľských rozhraní vývojového prostredia Eclipse Che. Najhlavnejšou prioritou tejto práce je zaistiť kompatibilitu testovacieho modulu pre Eclipse Che s testovacím modulom pre editor Visual Studio Code. Aby bolo možné zaistiť kompatibilitu medzi oboma editormi, bolo navrhnuté spoločné programátorské rozhranie pre grafické komponenty editorov. Vytvorené riešenie umožňuje vývojárom rozšírení editora Visual Studio Code používať testy grafického užívateľského rozhrania aj vo vývojovom prostredí Eclipse Che s minimálnymi úpravami. Prínosom tejto práce je zníženie nárokov na údržbu testov grafického rozhrania a jednotný zdrojový kód pre rozšírenie a testy., The goal of this thesis is to design and implement module for testing graphical user interfaces of integrated development environment Eclipse Che. The biggest priority of this thesis is to make the module compatible with module for testing graphical user interfaces of editor Visual Studio Code. In order to ensure compatibility between both editors, new module was created to define common application programming interface for graphical components. Created solution enables Visual Studio Code extension developers to use existing user interface tests in Eclipse Che IDE with minimal effort. As result source code can be shared which reduces maintenance costs.

Cílem bakalářské práce je vytvořit nástroj Suiter , který testerovi zjednoduší a částečně zautomatizuje proces tvorby testovacích skriptů v širokém spektru programovacích jazyků. Důraz je kladen na testování rozhraní pro programování aplikací ( API ) kombinováním vstupních hodnot v určitém stavu webové aplikace. Aplikace Suiter generuje spustitelnou sadu testů uspokojující požadovaná kombinační kritéria. Výsledky této práce umožňují testerům zrychlit a zefektivnit testování API ., The goal of this bachelor's thesis is to create a Suiter tool that partially automates the process of creating test scripts in a wide range of programming languages . The focus is given to a testing of application programming interface ( API ) by combining input values in a specific state of a web application . Suiter generates an executable set of tests that satisfy the required combination criteria .

Cílem této práce je automatizace přípravy testovacího prostředí v procesu manuálního včasného testování komponenty ovirt-web-ui projektu oVirt/RHV a umožnit tak testerovi efektivně využít svůj čas. Při řešení práce byly nastudovány agilní metodiky, princip včasného testování, projekt oVirt/RHV a nástroje Jira, Jenkins a GitHub usnadňující vývoj software. Automatizace byla implementovaná v jazyce Python a zasazena do existující automatizační struktury v GitLabu, přičemž je automaticky spouštěna pomocí nástroje Jenkins. Vytvořené komponenty pro komunikaci s jednotlivými nástroji umožňují nejen běh skriptu, který provádí přípravu prostředí, ale také budoucí získávání dat do databáze. Výsledná práce byla řádně otestována a podařilo se dosáhnout uvolnění až 2 hodin času testera na jiné pracovní aktivity., The objective of this work is to automate the preparation of a testing environment, which is a part of manual early testing of ovirt-web-ui component in project oVirt/RHV and allow the tester to work efficiently. Agile methods, early testing principles, project oVirt/RHV, and software development tools Jira, Jenkins, and GitHub were studied in this thesis. Automation was implemented in Python programming language and the work was incorporated into an existing automation structure in GitLab, while simultaneously being run by the Jenkins tool. All created components communicating with each software development tool are not only used in the preparation script but also will be utilized to gather data into the database in the future. The finished work was thoroughly tested and helped to free up to 2 hours of tester's time for other work-related activities.

Kontajnerové technológie sa v modernej dobe široko využívajú. Vo väčšine prevládajú aplikácie vytvorené na architektúre mikro služieb. Táto práca analyzuje návrh aplikácie, ktorá bude spracovávať údaje v reálnom čase. Aplikácia bude ďalej budovaná pomocou najmodernejších technológií používaných svetovými spoločnosťami ako Netflix, Uber. Používajú tieto systémy na spracovanie údajov v reálnom čase, ako je Apache Kafka, a v poslednom čase ich zavádzajú na vyššiu úroveň zapuzdrením tohto systému do kontajnerového prostredia, čo zaručuje ľahkú škálovateľnosť. Okrem toho využívaju najnovšie natívne technológie Kubernetes na spracovanie mnoho údajov pomocou programov Quarkus a Strimzi. Problém, ktorý sa objavuje, spočíva v tom, že testovanie týchto typov systémov na spracovanie údajov v reálnom čase uzavretých v kontajneroch je obzvlášť náročné. Hlavným cieľom práce je proof-of-concept aplikácie nad Strimzi testami. Táto práca tiež ukáže navrhnutý dlhodobý test applikácie a systému Strimzi, tiež známy ako Marathon, ktorý je ideálnou ukážkou užívateľských podmienok., Container technologies become broadly used in modern times. In prevailing, applications made on the micro-service architecture are rising. This thesis analyzes the design of an application that will process data in real-time. Further, the application will be built using state-of-the-art technologies used by world companies like Netflix, Uber. They are using the systems for real-time data processing such as Apache Kafka, and in recent times they raised it on a higher level by encapsulating this system in the container environment, which guaranteeing effortless scalability. Additionally, using the latest native Kubernetes technologies for processing dozens of data with Quarkus and Strimzi. The problem, which arises, is that these types of real-time data processing systems encapsulated in the containers are especially challenging to test. The main goal of this thesis is a proof-of-concept application based on Strimzi project and also show the designed long term test of the application also known as Marathon, which is the ideal demonstration of user conditions.

Mnoho aplikací přijímá, odesílá a zpracovává data v textové podobě. Správné a bezpečné zpracování těchto dat je typicky zajištěno tzv. ošetřením řetězců (string sanitization). Pomocí metod formální verifikace je možné analyzovat takovéto operace s řetězci a prověřit, zda jsou správně navržené či implementované. Naším cílem je vytvořit obecný nástroj pro analýzu systémů jejichž konfigurace lze kódovat pomocí slov z vhodné abecedy, a také jeho specializaci pro analýzu programů pracujících s řetězci. Nejprve jsou popsaný konečné automaty a převodníky a poté různé třídy a podtřídy symbolických převodníků, zejména pak jejich omezení. Na základě těchto informací je pak pro použití v analýze programů navržen nový typ symbolických převodníků. Dále je popsán regulární model checking, speciálně pak jeho variantu založenou na abstrakci automatů, tzv. ARMC, u kterého je známo že dokáže velmi úspěšně překonat problém stavové exploze u automatů a umožňuje nám tzv. dosáhnout pevného bodu v analýze. Poté je navržena vlastní analýza programů psaných v imperativním paradigmatu, a to zejména programů manipulujících s řetězci, založená na principech ARMC. Následuje popis vlastní implementace nástroje s důrazem na jeho praktické vlastnosti. Rovněž jsou popsaný důležité části knihovny AutomataDotNet, na které nástroj staví. Práci je uzavřena diskuzí experimentů s nástrojem provedených na příkladech z knihovny LibStranger., Many software applications receive, send and process data in a text form. Correct and safe processing of these data is usually ensured by so-called string sanitization. With the help of methods of formal verification, we can analyse these string operations and check whether they are correctly designed and implemented. The goal of this work is to create a tool for analysis of systems whose configurations can be encoded as words over a suitable alphabet, as well as its specialization for analysing string manipulating programs. First, we describe finite automata and transducers in general and characterize various classes and sub-classes of symbolic transducers, especially their limitations. Based on this study, a new class of symbolic transducers is proposed for use in the program analysis. Later, we introduce regular model checking, especially its variant based on abstraction over automata, the so called ARMC, which was proved to be able to quite successfully fight the state explosion problem in the size of the automata and allows us to reach a fix-point. We then design an analysis of programs written in imperative languages, especially those that manipulate strings, using the principles of ARMC. Finally, the implementation of the tool is presented, highlighting its practical aspects and discussing relevant parts of AutomataDotNet library it is based on. The work completes debating the experimental evaluation of the tool using test inputs from LibStranger project.

Táto práca sa zaoberá fuzz testovaním REST API. Po prezentovaní prehľadu techník používaných pri fuzz testovaní a posúdení aktuálnych nástrojov a výskumu zameraného na REST API fuzz testovanie, sme pristúpili k návrhu a implementácii nášho REST API fuzzeru. Základom nášho riešenia je odvodzovanie závislostí z OpenAPI formátu popisu REST API, umožňujúce stavové testovanie aplikácie. Náš fuzzer minimalizuje počet po sebe nasledujúcich 404 odpovedí od aplikácie a testuje aplikáciu viac do hĺbky. Problém prehľadávania dostupných stavov aplikácie je riešený pomocou usporiadania závislostí tak, aby sa maximalizovala pravdepodobnosť získania potrebných vstupných dát pre povinné parametre, v kombinácii s rozhodovaním, ktoré povinné parametre môžu využívať aj náhodne generované hodnoty. Implementácia je rozšírením Schemathesis projektu, ktorý generuje vstupy za pomoci Hypothesis knižnice. Implementovaný fuzzer je použitý na testovanie Red Hat Insights aplikácie, kde našiel 32 chýb, z čoho jednu chybu je možné reprodukovať len za pomoci stavového testovania., This thesis is dealing with fuzz testing of REST API. After presenting state-of-the-art of fuzzing and assessing the current research regarding REST API fuzz testing, we design and implement our REST API fuzzer. The proposed fuzzer infers dependencies of API calls defined in an OpenAPI specification and makes the fuzzing stateful. One of the features is minimization of the number of successive 404 responses while maintaining exploration of a deeper state space of a tested application. To solve the exploration vs. exploitation problem, we used the ordering of dependencies maximizing the probability of obtaining a needed input values and determining of fuzzability of a required parameters. The implementation is an enhancement of the Schemathesis project that is using the Hypothesis library to randomly generate inputs. Our fuzzer is evaluated against the Red Hat Insights application, finding 32 bugs. Amid them, one bug is reproducible only by a stateful set of steps.

Testování multikomponentních IT a IoT systémů, které zpracovávají proudy různých zpráv je složitou úlohou. Proč je to složité? Kvůli množství komponentů, jejích asynchronní interakcí, různým kombinacím události pro testování, testovacímu prostředí, které se liší od reálného a množství dalším důvodů. Táhle práce navrhuje způsob generování komplexních dat pro testovací účely s minimálním zásahem vývojářů. Generování dat založeno na analýze sledu komunikace reálného systému a následnou syntézou podobných sledů pro testování. Práce také navrhuje framework na prvotní analýzu zpráv přenášených v zachycené komunikace. Tohle může být uděláno použitím různých abstraktních modelů: modelu zprávy a modelu komunikaci. Výsledkem téhle práce je implementovaní knihovna na tvorbu modelu zprávy a množina operací pro práci s tímto modelem., Testing multicomponent systems in IT and IoT that process the streams of different messages is a complicated task. Why it is complicated? Because of the number of components, asynchronous interaction, different combinations of actions to test, test environment differs from the real environment and others. This thesis introduces an idea of how to generate complex input data for system testing while requiring minimum intervention from a developer. The test data generation is based on the analysis of traces of communication in a real system, and the reproduction of similar traces for testing purposes. The paper also proposes a framework for the initial analysis of messages transferred within the recorded communication. It can be solved using different abstract models: the message model, the communication model. The result of this work is the implemented library for creating a message model with a set of operations for working with this model.

Tato práce rozšiřuje nástroj ANaConDA pro dynamickou analýzu vícevláknových programů o možnost analyzovat také programy víceprocesové. Část práce se soustředí na popis nástroje ANaConDA a mechanismů, které pro monitorování využívá, a na jejich nutné úpravy vzhledem k rozdílům procesů a vláken. Tyto zahrnují nutnost složitějších mechanismů pro meziprocesovou komunikaci, nutnost překládat logické adresy na jiný jednoznačný identifikátor a monitorování obecných semaforů. Rozšíření pro monitorování procesů tyto problémy řeší za vývojáře analyzátorů, čímž velmi zjednodušuje jejich vývoj. Užitečnost rozšíření je ukázána na implementaci dvou analyzátorů pro detekci souběhu (AtomRace a FastTrack), které bylo dosud možné využít pouze na vícevláknové programy. Implementace algoritmu FastTrack využívá happens-before relaci pro obecné semafory, která byla také definována jako součást této práce. Experimenty s analyzátory na studentských projektech ukázaly, že nástroj ANaConDA je nyní schopen detekovat paralelní chyby i ve víceprocesových programech a může tak pomoci při vývoji další skupiny paralelních programů., This work extends ANaConDA framework for dynamic analysis of multi-threaded programs with support for multi-process monitoring. This thesis summarizes ANaConDA's approach to analysis and differences between threads and processes. The most important ones involve inter-process communication, separate logical address spaces, and synchronisation with general semaphores. The implemented extension provides API for inter-process communication via shared memory, monitors operations with shared memory in order to translate virtual addresses to their unique representation among processes, and monitors synchronisation operations with semaphores and provides information about them to analysers. The extension significantly simplifies the development of multi-process analysers. This is shown on implementation of two analysers for data race detection, AtomRace and FastTrack, which were, until now, available for multi-threaded programs only. The implementation of FastTrack algorithm uses happens-before relation for general semaphores which is also defined in this thesis. Proposed and implemented solutions were verified on a set of automatic tests and the two analysers were used for experiments on a set of students' projects. Experiments showed that ANaConDA framework is now able to detect concurrency-related errors in multi-process programs and, as such, provide support with implementation of large category of parallel programs.

Tato práce rozšiřuje nástroj ANaConDA pro dynamickou analýzu vícevláknových programů o možnost analyzovat také programy víceprocesové. Část práce se soustředí na popis nástroje ANaConDA a mechanismů, které pro monitorování využívá, a na jejich nutné úpravy vzhledem k rozdílům procesů a vláken. Tyto zahrnují nutnost složitějších mechanismů pro meziprocesovou komunikaci, nutnost překládat logické adresy na jiný jednoznačný identifikátor a monitorování obecných semaforů. Rozšíření pro monitorování procesů tyto problémy řeší za vývojáře analyzátorů, čímž velmi zjednodušuje jejich vývoj. Užitečnost rozšíření je ukázána na implementaci dvou analyzátorů pro detekci souběhu (AtomRace a FastTrack), které bylo dosud možné využít pouze na vícevláknové programy. Implementace algoritmu FastTrack využívá happens-before relaci pro obecné semafory, která byla také definována jako součást této práce. Experimenty s analyzátory na studentských projektech ukázaly, že nástroj ANaConDA je nyní schopen detekovat paralelní chyby i ve víceprocesových programech a může tak pomoci při vývoji další skupiny paralelních programů., This work extends ANaConDA framework for dynamic analysis of multi-threaded programs with support for multi-process monitoring. This thesis summarizes ANaConDA's approach to analysis and differences between threads and processes. The most important ones involve inter-process communication, separate logical address spaces, and synchronisation with general semaphores. The implemented extension provides API for inter-process communication via shared memory, monitors operations with shared memory in order to translate virtual addresses to their unique representation among processes, and monitors synchronisation operations with semaphores and provides information about them to analysers. The extension significantly simplifies the development of multi-process analysers. This is shown on implementation of two analysers for data race detection, AtomRace and FastTrack, which were, until now, available for multi-threaded programs only. The implementation of FastTrack algorithm uses happens-before relation for general semaphores which is also defined in this thesis. Proposed and implemented solutions were verified on a set of automatic tests and the two analysers were used for experiments on a set of students' projects. Experiments showed that ANaConDA framework is now able to detect concurrency-related errors in multi-process programs and, as such, provide support with implementation of large category of parallel programs.

Táto práca sa zaoberá fuzz testovaním REST API. Po prezentovaní prehľadu techník používaných pri fuzz testovaní a posúdení aktuálnych nástrojov a výskumu zameraného na REST API fuzz testovanie, sme pristúpili k návrhu a implementácii nášho REST API fuzzeru. Základom nášho riešenia je odvodzovanie závislostí z OpenAPI formátu popisu REST API, umožňujúce stavové testovanie aplikácie. Náš fuzzer minimalizuje počet po sebe nasledujúcich 404 odpovedí od aplikácie a testuje aplikáciu viac do hĺbky. Problém prehľadávania dostupných stavov aplikácie je riešený pomocou usporiadania závislostí tak, aby sa maximalizovala pravdepodobnosť získania potrebných vstupných dát pre povinné parametre, v kombinácii s rozhodovaním, ktoré povinné parametre môžu využívať aj náhodne generované hodnoty. Implementácia je rozšírením Schemathesis projektu, ktorý generuje vstupy za pomoci Hypothesis knižnice. Implementovaný fuzzer je použitý na testovanie Red Hat Insights aplikácie, kde našiel 32 chýb, z čoho jednu chybu je možné reprodukovať len za pomoci stavového testovania., This thesis is dealing with fuzz testing of REST API. After presenting state-of-the-art of fuzzing and assessing the current research regarding REST API fuzz testing, we design and implement our REST API fuzzer. The proposed fuzzer infers dependencies of API calls defined in an OpenAPI specification and makes the fuzzing stateful. One of the features is minimization of the number of successive 404 responses while maintaining exploration of a deeper state space of a tested application. To solve the exploration vs. exploitation problem, we used the ordering of dependencies maximizing the probability of obtaining a needed input values and determining of fuzzability of a required parameters. The implementation is an enhancement of the Schemathesis project that is using the Hypothesis library to randomly generate inputs. Our fuzzer is evaluated against the Red Hat Insights application, finding 32 bugs. Amid them, one bug is reproducible only by a stateful set of steps.

Tato práce představuje optimalizační techniky zaměřené na proces sběru výkonnostních dat v rámci výkonnostní analýzy a profilování programů v nástroji Perun. Rozšíření architektury a implementace těchto nových optimalizačních technik v nástroji Perun (a převážně pak v jeho modulu Tracer) zlepšuje jeho škálovatelnost a umožňuje tak provádět výkonnostní analýzu i nad rozsáhlými projekty. Zaměřujeme se především na zvýšení přesnosti sběru dat, redukci množství instrumentovaných bodů programu, omezení časové režie procesu sběru dat a výkonnostního profilování, snížení objemu sbíraných dat a velikosti výsledného výkonnostního profilu. Optimalizace je dosažena pomocí aplikace statistických metod, množství technik statické a dynamické analýzy (případně jejich kombinací) a využitím pokročilých možností a schopností nástrojů SystemTap a eBPF. Na základě vyhodnocení provedeného na dvou vybraných projektech a množství experimentů můžeme konstatovat, že se nám úspěšně podařilo dosáhnout značné optimalizace u téměř všech sledovaných metrik a kritérií., In this work, we propose optimization techniques focused on the data collection process of program performance analysis and profiling within the Perun framework. We enhance Perun (and especially its Tracer module) by extending their architecture and implementing novel optimization techniques that allow Perun to scale well even for large projects and test scenarios. In particular, we focus on improving the data collection precision, scaling down the amount of injected instrumentation, limiting the time overhead of the collection and profiling processes, reducing the volume of raw performance data and the size of the resulting profile. To achieve such optimization, we utilized statistical methods, several static and dynamic analysis approaches (as well as their combination) and exploited the advanced features and capabilities of SystemTap and eBPF frameworks. Based on the evaluation performed on two selected projects and numerous experiment cases, we were able to conclude that we successfully achieved significant levels of optimization for nearly all of the identified metrics and criteria.

Testování multikomponentních IT a IoT systémů, které zpracovávají proudy různých zpráv je složitou úlohou. Proč je to složité? Kvůli množství komponentů, jejích asynchronní interakcí, různým kombinacím události pro testování, testovacímu prostředí, které se liší od reálného a množství dalším důvodů. Táhle práce navrhuje způsob generování komplexních dat pro testovací účely s minimálním zásahem vývojářů. Generování dat založeno na analýze sledu komunikace reálného systému a následnou syntézou podobných sledů pro testování. Práce také navrhuje framework na prvotní analýzu zpráv přenášených v zachycené komunikace. Tohle může být uděláno použitím různých abstraktních modelů: modelu zprávy a modelu komunikaci. Výsledkem téhle práce je implementovaní knihovna na tvorbu modelu zprávy a množina operací pro práci s tímto modelem., Testing multicomponent systems in IT and IoT that process the streams of different messages is a complicated task. Why it is complicated? Because of the number of components, asynchronous interaction, different combinations of actions to test, test environment differs from the real environment and others. This thesis introduces an idea of how to generate complex input data for system testing while requiring minimum intervention from a developer. The test data generation is based on the analysis of traces of communication in a real system, and the reproduction of similar traces for testing purposes. The paper also proposes a framework for the initial analysis of messages transferred within the recorded communication. It can be solved using different abstract models: the message model, the communication model. The result of this work is the implemented library for creating a message model with a set of operations for working with this model.

Cílem této práce bylo vytvořit virtuální stroj, emulující spouštění programů napsaných v programovacím jazyce Java, který by byl vhodný pro analýzu a detekci malware. Emulátor je schopen zjistit argumenty zneužitelných metod standardních tříd jazyka Java, pořadí volání těchto zneužitelných metod a také vlastní provedení testované aplikace. Celková funkcionalita byla otestována na vhodných příkladech, na kterých proběhlo i vlastní měření. V závěru práce je popsáno testování celkového řešení, kde jsou také uvedeny tabulky a grafy pro lepší znázornění dosažených výsledků., The goal of this thesis is to create a virtual machine that emulates a running programs written in Java programing language, which would be suitable for malware analysis and detection. The emulator is able to detect arguments of exploitable methods from Java standard classes, the order of calling these exploitable methods and also execution the test application. Overall functionality was tested on appropriate examples in which held its own measurements. At the end of the paper we describe testing of the emulator, which also contains tables and graphs for better results visualization.

Konečné stromové automaty jsou formalismem používaným v mnoha různých oblastech informatiky, mimo jiné v oblasti formální verifikace. V současné době existuje několik nástrojů pro práci s konečnými stromovými automaty, avšak knihovny nástroje MONA jsou pro tyto účely nejlepší. Právě konečné stromové automaty jsou častým nástrojem pro formální verifikaci počítačových systémů, které pracují s dynamickými datovými strukturami. Způsob, jakým je realizováno zadávání konečných stromových automatů pro knihovny nástroje MONA , je pro člověka značně náročný, protože je nutné funkci přechodu konečného stromového automatu zadat ve formě několika multiterminálních binárních rozhodovacích diagramů. Cílem této diplomové práce je navrhnout a implementovat nástroj pro převod konečných stromových automatů zapsaných výčtem pravidel do interního formátu nástroje MONA ., Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.

Konečné stromové automaty jsou formalismem používaným v mnoha různých oblastech informatiky, mimo jiné v oblasti formální verifikace. V současné době existuje několik nástrojů pro práci s konečnými stromovými automaty, avšak knihovny nástroje MONA jsou pro tyto účely nejlepší. Právě konečné stromové automaty jsou častým nástrojem pro formální verifikaci počítačových systémů, které pracují s dynamickými datovými strukturami. Způsob, jakým je realizováno zadávání konečných stromových automatů pro knihovny nástroje MONA , je pro člověka značně náročný, protože je nutné funkci přechodu konečného stromového automatu zadat ve formě několika multiterminálních binárních rozhodovacích diagramů. Cílem této diplomové práce je navrhnout a implementovat nástroj pro převod konečných stromových automatů zapsaných výčtem pravidel do interního formátu nástroje MONA ., Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.

Cílem této práce bylo vytvořit virtuální stroj, emulující spouštění programů napsaných v programovacím jazyce Java, který by byl vhodný pro analýzu a detekci malware. Emulátor je schopen zjistit argumenty zneužitelných metod standardních tříd jazyka Java, pořadí volání těchto zneužitelných metod a také vlastní provedení testované aplikace. Celková funkcionalita byla otestována na vhodných příkladech, na kterých proběhlo i vlastní měření. V závěru práce je popsáno testování celkového řešení, kde jsou také uvedeny tabulky a grafy pro lepší znázornění dosažených výsledků., The goal of this thesis is to create a virtual machine that emulates a running programs written in Java programing language, which would be suitable for malware analysis and detection. The emulator is able to detect arguments of exploitable methods from Java standard classes, the order of calling these exploitable methods and also execution the test application. Overall functionality was tested on appropriate examples in which held its own measurements. At the end of the paper we describe testing of the emulator, which also contains tables and graphs for better results visualization.

Tato disertační práce představuje derivační stromy několika různých typů gramatik ve zobecněné Kurodově normální formě; jmenovitě obecné a regulárně řízené gramatiky, gramatiky s rozptýleným kontextem a spolupracující distribuované gramatické systémy. Definuje jednoduché stromové rysy založené na kontextových vlastnostech jednotlivých diskutovaných gramatik a dokazuje, že pokud existuje limitující konstanta k taková, že každá věta generovaného jazyka L odpovídá řetězci listových uzlů derivačního stromu, ve kterém je výskyt definovaných stromových rysů omezen konstantou k, jazyk L je ve skutečnosti bezkontextový. Tato práce dále ukazuje, že dosažený výsledek představuje silný nástroj důkazu bezkontextovosti jazyka. Vše je doplněno příklady praktického využití nástroje., The present thesis introduces derivation trees for several different types of grammars in generalized Kuroda normal forms; namely, general, regular-controlled, and scattered context grammars and cooperating distributed grammar systems. It defines simple tree-based properties related to non-context-free properties of all grammars in question and shows that if there exists a limiting constant k such that every sentence in the generated language L is the frontier of a derivation tree in which the number of occurrences of the defined tree-based properties is limited by k, the language L is in fact context-free. The thesis explains that this result represents a powerful tool for showing languages to be context-free. It also provides illustrations and examples which sketch how to apply this tool in practice.

Integračné testovanie prebieha v projekte Beaker vždy v čistom prostredí, na čerstvo nainštalovanom operačnom systéme. Inštalácia zaberá veľké percento z doby prípravy testovacieho stroja. Táto práca sa snaží o urýchlenie daného procesu prípravy pomocou klonovania obrazov diskov virtuálnych strojov na platforme OpenStack. Pre beh testov na tejto platforme je nutné aby mal Beaker vlastný OpenStack účet, nainštalované knižnice potrebné pre komunikáciu, aby boli obrazy diskov vopred nahraté do cloudu a aby testovacia sada vyžadovala beh na procesorovej architektúre x86_64. Očakáva sa, že toto vylepšenie prinesie urýchlenie prípravy testovacích strojov a tým pádom aj urýchlenie testovania a zvýšenie efektivity využitia výpočetných zdrojov. Výsledok práce má praktické využitie pre firmu Red Hat, ktorá ho plánuje používať pri pravidelnom testovaní balíčkov., Integration testing in Beaker project is always performed in a clear environment, on a freshly installed operating system. The installation takes up a large percentage of the test machine preparation time. This work attempts to accelerate the process of preparation by cloning virtual machine images in OpenStack cloud platform. In order to run tests on this platform, Beaker must have it's own OpenStack account, some extra libraries installed on the Beaker server side, images must be uploaded into cloud in advance and the tests must require x86_64 cpu architecture. This feature is expected to accelerate the preparation of test machines and thus accelerate testing and increase the efficiency of computing resources usage. The result of this work is planned to be used by Red Hat for regular package testing.

Tato bakalářská práce pojednává o návrhu a implementaci prodejního internetového informačního systému, který umožňuje objednávat zboží (jako tradiční elektronický obchod) a vést veškerou agendu spojenou s vyřizováním těchto objednávek. Tento systém zároveň implementuje funkce, které zjednodušují provozovateli chod internetového obchodu (vedení skladové evidence, fakturace, expedice). Zabývá se návrhem a implementací SEO optimalizované aplikace, která je zároveň plně lokalizovaná. Tato bakalářská práce se dále zabývá moderními prvky tvorby webových aplikací, které byly při návrhu a implementaci systému použity (frameworky, databázové mappery apod.), This bachalor's thesis discusses design and implementation of internet-based sales system that allows ordering goods (such as traditional e-commerce) and keep all the work connected with the processing of orders. This system also implements features that help owner with leading this e-commerce (keeping stock records, billing, shipping). It deals with the design and implementation of SEO-friendly application, which is also fully localized. This thesis also deals with modern elements of web applications, which are base of this system (frameworks, database mappers, etc.)

Táto diplomová práca sa zaoberá analýzou dynamických dátových štruktúr pomocou analýzy tvaru použitej v nástroji Predator. Popisuje zvolenú abstraktnú doménu pre reprezentáciu pamäte vo forme symbolických grafov pamäte. Ďalej sa zaoberá návrhom prostredia pre vývoj statických analyzátorov nad clang/LLVM. Prínosom tejto práce je vytvorenie a otestovanie transformačných priechodov zjednodušujúcich LLVM IR medzikód. Ďalším prínosom je optimalizácia parametrov paralelnej nadstavby Predatora opakovaným spúšťaním testov z medzinárodnej súťaže SV-COMP'16, kde táto verzia nástroja Predator získala zlatú medailu v kategórii Heap Data Structures. Posledným prínosom je návrh architektúry samotného verifikačného jadra s ohľadom na SMG doménu., This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.

Statická analýza se v současnosti dostává do popředí v oblasti technik pro odhalování chyb v moderním software. Nedostatečná škálovatelnost, především v kombinaci se zachováním potřebné přesnosti, je však přetrvávající problém u většiny současných nástrojů pro statickou analýzu, což je činí nepoužitelnými v případě rozsáhlého a často se měnícího kódu. Efektivní statické analyzátory, jako například Coverity nebo Code Sonar, jsou navíc často proprietární a není tedy možné je jednoduše rozšířit nebo srovnávat jejich výsledky. Oproti tomu Facebook Infer nabízí open source rámec s důrazem na kompoziční, inkrementální, a v důsledku i škálovatelnou inter-procedurální statickou analýzu. Tato práce představuje Looper --- nový analyzátor zaměřující se na analýzu výkonnosti, přesněji na analýzu mezí, rozšiřující rámec nástroje Facebook Infer. Implementace našeho analyzátoru je založena na existujícím nástroji Loopus, který se zaměřuje na přesnou analýzu mezí. Výsledný prototyp jsme otestovali na dvou různých testovacích sadách a povzbudivé výsledky srovnali s existujícím analyzátorem Cost, který je vyvíjen Infer týmem., Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, reasonably precise static analysis tools still often struggle to scale well on large and quickly changing codebases. Efficient static analysers, such as Coverity or Code Sonar, are usually proprietary and difficult to openly evaluate or extend. On the contrary, Facebook Infer offers an open source static analysis framework with the emphasis on compositional, incremental and consequently highly scalable inter-procedural analysis. This thesis presents Looper --- a new performance oriented resource bounds analyser which extends the capabilities of Facebook Infer. We have based our implementation on an existing resource bounds analyser Loopus and evaluated it on two different test suites, showing encouraging results in comparison with the existing Cost analyser developed by the Infer team.

Statická analýza dnes patrí medzi najpopulárnejšie metódy na odhaľovanie chýb v modernom softvéri, no častým problémom dostatočne presných statických analyzátorov je ich škálovateľnosť. Mnohé efektívne analyzátory (napr.:Coverity, KlockWork, atď.) sú navyše proprietárne, čím sa ich ďalšia rozšíriteľnosť a použitie stávajú obťažnými. Pokrok v tejto oblasti prináša Facebook Infer, ktorý ponúka open-source framework na tvorbu kompozičných a inkrementálnych statických analýz. V tejto práci predstavujeme vlastný Low-Level Deadlock Detector (L2D2), ktorý rozširuje funkcionalitu Inferu. Náš algoritmus spĺňa princípy kompozičnej analýzy, založenej na kontextovo nezávislom výpočte súhrnu pre každú funkciu, čo má za následok jeho vysokú škálovateľnosť. Algoritmus sme implementovali a overili na sade príkladov z Debian GNU/Linux, ktorá pozostávala z 11.4 MLOC. Aj keď náš prístup nie je ani presný ani úplný, ukazuje sa ako efektívny. Okrem toho, že dokázal odhaliť všetky známe uviaznutia, hlásil falošné pozitíva v menej ako 4% z testovaných programov., Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.

Testovanie výkonu predstavuje kľúčový faktor pri optimalizácii programov počas ich vývoja, avšak, v súčastnosti nie je vyvinutý na takej úrovni ako funkcionálne testovanie. Nástroj Perun poskytuje automatickú správu výkonnosti programov, čím prispieva k vývoju tejto oblasti. V tejto práci predstavujeme tri neparametrické prístupy modelovania výkonnostných dát: regresogram, kĺzavý priemer a jadrové odhady, ktoré boli integrované v rámci tohto nástroja. Použitím týchto techník sa snažíme dosiahnuť vhodnú aproximáciu výkonnostných dát bez predpokladu závislosti medzi dvoma premennými, čo predstavuje hlavnú výhodu oproti aktuálne používaným parametrickým technikám. V rámci tohto nástroja, sme tiež navrhli a implementovali dve metódy pre automatickú detekciu degradácie výkonu, ktoré dokážu pracovať so všetkými druhmi modelov. Riešenie sme demonštrovali na reálnom projekte ( Vim) a na sade experimentálnych prípadov, v ktorých sme navrhnuté riešenia porovnali s už existujúcimi. Novými prístupmi modelovania sme dosiahli zvýšenú časovú efektivitu o dve tretiny a priemerne trojnásobne lepšiu presnosť modelovania dát. Navrhnuté metódy detekovali degradáciu výkonu troch špecifických funkcií v porovnaní dvoch verzií programu Vim , kde bola prítomná ohlásená výkonnostná chyba., Performance testing is a critical factor in the optimisation of programs during its development, but it is still not so well developed in comparison to functional testing. A framework Perun provides full automation of performance management, thereby contributing to the development of this area. We have introduced three non-parametric approaches to performance data modelling: regressogram, moving average and kernel regression, which were integrated within this framework. We try to achieve appropriate approximations of performance data using these techniques, without the assumption of dependence between two variables, which represents the main advantage in comparison to parametric techniques. Further, we have proposed and implemented two methods for automatic detection of performance changes, which works with all kinds of models within Perun . We have demonstrated our solutions on the real project ( Vim ), and on the set of the experimental cases, in which we compared proposed solutions with existing. We have achieved decreased time processing about two-thirds and an almost triple improvement in the fitness of data modelling with new modelling approaches. The proposed detection methods detected performance degradation of three specific functions in comparison of two different versions of Vim, where was present a known performance issue.

Výkon plánovače procesů v jádře operačního systému značně ovlivňuje rychlost a odezvu všech aplikací, které na něm běží. Jakýkoli propad výkonu pak může mít kritické důsledky na běhu aplikací. S příchodem každé nové technologie (např. symetrický multiprocesing) se kód plánovače vyvíjí a rozšiřuje. Proto jsou potřeba regresní testy nejen na jeho fukčnost, ale i výkon. Tato práce mapuje metody testování plánovače operačního systému Linux ve firmě Red Hat. Popisuje způsoby měření výkonu plánovače, sbírání informací o jeho chování, ukládání sesbíraných dat a jejich vizualizaci. Hlavním cílem práce je pak návrh a implementace nového způsobu vizualizace dlouhodobých měření a využití strojového učení pro automatické rozpoznání degradace výkonu mezi dvěma výsledky., Performance of process scheduler in a kernel of an operating system significantly influences throughput and latency of all applications running above it. Any performance drop can have critical consequences on the applications. With the arrival of every new technology (e.g. symetric multiprocesing) the code of the scheduler evolves and grows. This requires not only functional, but also performance regression testing. This work presents methods of performance testing used in the Red Hat, Inc. company. It describes how one can measure performance of the Linux process scheduler in the Linux kernel, collect statistics about its behavior, store the collected data, and visualize them. The goal of this work is to design and implement a new technique of visualization of long-term measurements and utilization of machine learning for automatic classification of performance degradation between different results.

Cieľom bakalárskej práce je vytvorenie systému na automatizované testovanie GUI desktopových aplikácií, ktorý sa dá jednoducho nasadiť ako testovacie prostredie. Tento systém pozostáva z nástroja, v ktorom je užívateľ schopný vytvárať testovacie skripty, a interpretu, ktorý spúšťa dané testovacie skripty a vyhodnocuje ich. Testovacie skripty užívateľ vytvára pomocou jazyka, ktorý je tiež popísaný v tejto práci. Jednoduché nasadenie systému zabezpečuje použitie kontajnerovej virtualizácie., The aim of this Bachelor thesis is to create a system for automated testing of GUI desktop applications that may be easily used as a test environment. The system consists of, first, an application in which the user is able to create the test scripts, and second, the interpreter that runs and evaluates the relevant test scripts. The user creates the test scripts using a~language that is also described in this thesis. Simple deployment of the system ensures the use of container-based virtualization.

Tato práce se zabývá detekováním skrytých prostředků v prostředí operačních systémů GNU/Linux. Současně analyzuje nástroje, které toto skrývání provádějí (tzv. rootkity). Práce je rozdělena na teoretickou a praktickou část. Teoretická část se zaměřuje především na způsob správy a reprezentace prostředků v operačním systému, režimy běhu a systémová volání. Praktická část se zabývá návrhem a implementací obecného detektoru, kterému jsou jednotlivé metody detekce předány formou zásuvných modulů. Některé z těchto metod jsou realizovány jako moduly jádra operačního systému. Účinnost detektoru je porovnána oproti reálným rootkitům., The main goal of this thesis was to detect hide resources in GNU/Linux operating systems and analyse tools so called rootkits, which are used to hide system resources. This thesis is devided into two parts, theoretical and practical one. Theoretic part focusses on resource managment, representation, privilege levels and system calls. Practical part covers design and implementation of an abstract detector. Each new detection method is implemented as a plugin. Some of those methods are realized as linux kernel modules. The usability of the detector is compared against real rootkits.

Tato bakalářská práce se zabývá návrhem a implementací nástroje pro editaci a simulaci Objektově orientovaných Petriho sítí. Nástroj podporuje dva formáty zápisu Objektově orientovaných Petriho sítí, a to PNtalk a PNML. Výsledná aplikace v jazyku Java poskytuje dvě hlavní skupiny funkcionalit - vytvářet, načítat a ukládat sítě v těchto formátech a vzdáleně spolupracovat se simulátorem a s jeho využitím zjistit stav simulace a zobrazit ho. První část práce je věnovaná teorii, v které jsou objasněné koncepty spojené s Objektově orientovanými Petriho sítěmi. Ve druhé části se zabýváme popisem implementace a funkcionality implementovaného nástroje pro editaci OOPN a způsobem propojení nástroje se simulátorem., This bachelor thesis deals with the design and implementation of the tool, which allows to edit and simulate Object oriented Petri nets. It supports two formats of Object oriented Petri nets, PNtalk and Petri Net Markup Language. The final tool implemented in Java programming language allows to create, save and load Petri nets in these formats, as well as to remotely cooperate with the simulator and display the simulation state. The first part of this thesis is devoted to theory. Concepts associated with Object oriented Petri nets are explained in the first part. The second part describes the implementation and functionality of the implemented editing tool and the process of connecting the editor with the simulator.

Tato práce se zabývá P/T Petriho sítěmi a jazyky Petriho sítí. V práci jsou také uvažovány omega-jazyky a jejich vztak k Petriho sítím. Hlavní náplní práce je navržení akceptoru (rozšířené Petriho sítě) některých tříd jazyků Petriho sítí včetně implementace akceptoru těchto tříd jazyků. V práci jsou popsány algoritmy použité při implementaci (rozlišení typu jazyka, automarické vyhodnocení přijetí řetězce, generování řetězců). Na testech je demonstrována správná funkce akceptoru., In this document P/T Petri nets and Petri nets languages are described. In this document omega-languages and relationship of omega-languages and Petri nets is also described. Main focus is set on design of acceptor (extended Petri net) of some classes of Petri nets languages and implementation of acceptor of this classes. Algorithms (recognition of language type, automatical accepting of string, strings generating) used in implementation of acceptor are described. Correct function of acceptor is demonstrated on tests.

Tato práce se zabývá standardem SCAP používaným v oblasti počítačové bezpečnosti a popisuje jeho svobodnou implementaci OpenSCAP. V textu je analyzován jazyk OVAL sloužící pro popis zraniteností a bezpečné konfigurace systémů. Důraz je kladen na typické problémy tohoto jazyka. Na základě získaných poznatků je navrženo rozšíření projektu OpenSCAP o možnost reportování a diagnostiky průběhu interpretace jazyka OVAL. Práce následně popisuje implementaci, integraci a testování tohoto rozšíření., This thesis deals with the SCAP standard, used in area of computer security, and describes its open source implementation OpenSCAP. The analysis focuses on OVAL, a language for determining vulnerabilities and configuration issues on computer systems. Typical problems of OVAL are discussed. Based on obtained findings, an extension of the OpenSCAP project for reporting and diagnostics of OVAL interpretation has been designed. The thesis describes implementation, integration and testing of proposed extension.

Cílem bakalářské práce bylo seznámení se s problematikou komunitných systémů, současných systémů na podporu výuky cizích jazyků, a na základě získaných poznatků navrhnout a implementovat komplexní výukový systém, umožňující nejen výuku s využitím efektivních metod učení se, ale i rozvoj systému komunitou uživatel. Při implementaci byli využity moderní technologie J2EE: Apache Wicket a Hibernate. Výsledný systém je přenosný a jednoduše nasaditeľný na aplikační server Apache Tomcat, v případě využití větší komunitou je možné použít placený Sun Java Aplication Server. Testování implementovaného systému na veřejně dostupném serveru FIT VUT proběhlo na vzorce 60 studentů a jeho výsledky jsou uvedeny v závěru práce., Main goal of this thesis is to analyze the current community and language learning systems and based on this analysis, to create a complex learning system. The system is implemented by modern J2EE technologies such as wickets and OR mapping. The final J2EE application is portable and easy to install on free Apache Tomcat application server or paid SUN application server. System was deployed on public FIT VUT server and tested by a sample of 60 students. Results and review of testing are at the end of this thesis.

Cloudová řešení získávají na popularitě, spolu s tím však roste jejich složitost. Pro jejich efektivní správu a řízení existují různá řešení. Projekt ManageIQ je jedním z těchto nástrojů. Tato bakalářská práce se zabývá integrací nového poskytovatele cloudové infrastruktury, IBM SoftLayeru, do prostředí správce cloudových řešení ManageIQ. Na tomto příkladě je vysvětleno, jaká rozhraní je třeba použít pro správu poskytovatelů, jak pracovat s cloudovými API a jaké výzvy je třeba řešit při integraci nového poskytovatele. Výsledkem práce je funkční prostředí umožnující snadnou práci v IBM SoftLayeru skrze ManageIQ. To uživateli zprostředkovává sledování a úpravy dostupných zařízení či vytváření a spouštění nových součástí infrastruktury., As cloud computing gains its popularity the complexity of offered services is growing. There exist various different solutions and to manage them effectively is the task for cloud managers. One of them is a project named {ManageIQ}. This thesis aims to describe how to integrate a new provider into this software, what are the required bindings and how to work with the API of the provider. This thesis describes such a process on an IBM SoftLayer provider example. The achieved result enables the user to manage his SoftLayer devices via ManageIQ with ease and also provides him the functionality to provision new appliances.

Tato práce se zabývá analýzou možností zálohování a verzování konfiguračních souborů pod operačním systémem GNU/Linux. Na základě zjištěných skutečností je navržen, implementován a otestován nový nástroj pro distribuci Fedora. Jeho cílem je zachovat výhody existujích řešení a odstranit jejich nedostatky. Také přináší nové užitečné funkce, jako je synchronizace se vzdáleným serverem a možnost integrace do jiných nástrojů pro správu., This thesis deals with current possibilities of creating backups and versioning of configuration files in GNU/Linux operating system. Based on the findings a new tool for Fedora distribution was designed, implemented, and tested. The aim of the tool is to keep the benefits of existing solutions and to eliminate their drawbacks. In addition, it brings some new and useful features like synchronization with remote server and integration with other management tools.

Cílem této bakalářské práce je zlepšení integrace mezi SUDO a SSSD se zaměřením na vylepšení podpory SUDO pravidel uložených na serveru FreeIPA. Zabývá se popisem LDAP SUDO provideru a prezentuje návrh a implementaci IPA SUDO providera. Navržený provider eliminuje nadbytečnou režii překládání SUDO pravidel z IPA SUDO schématu do nativního LDAP SUDO schématu na straně FreeIPA serveru., The purpose of this thesis is to improve integration between SUDO and SSSD with a fo- cus on improved support of SUDO rules stored on an FreeIPA server in the native IPA SUDO scheme. It presents documentation of LDAP SUDO provider and also the design and implementation of a native IPA SUDO provider. The designed provider eliminates an unnecessary overhead of exporting SUDO rules from IPA SUDO schema to native LDAP SUDO scheme on an FreeIPA server.

Bakalářská práce se zabývá problematikou umělé inteligence v počítačové hře. V práci je uveden návrh dvourozměrné počítačové hry pro dva hráče, kde jednoho z nich může řídit počítač. Hlavní úlohou bylo vytvoření hry s jednoduchým uživatelským rozhraním, se zaměřením na umělou inteligenci soupeře., This Bachelor's thesis is focused on artificial intelligence in computer games. It introduces the design of a two-dimensional computer game for two players of which one can be computer-controlled. The main task was the creation of a game with a simple user interface with focus on the opponent's artificial intelligence.

Cílem této práce je vytvoření webové aplikace pro správu elektronické knihovny, která vytváří webové rozhraní nad programem Calibre. Při tvorbě bylo dbáno na to, aby byl výsledek dále jednoduše rozšiřitelný a přístupný širokému okruhu uživatelů. Základem systému je jazyk PHP a knihovna Nette Framework. Text této práce popisuje kompletní vývojový cyklus aplikace od rozboru současného stavu přes analýzu požadavků, návrh systému a návrh uživatelského rozhraní až po implementační detaily a rozbor testování na vzorku uživatelů., The aim of this work is to create a web application for ebook library management which builds a web interface around Calibre. A particular focus was given to extensibility and accessibility for a large spectrum of users. The base of the system is the PHP programming language and the Nette Framework library. The text of this thesis describes the complete development process from the analysis of current situation, requirements analysis, system design and user interface design to implementation details and the analysis of testing on a sample of users.

WildFly je platformou pro distribuované prostředí splňující specifikaci Java Enterprise Edition. Tato práce se zabývá možnostmi centrální správy bezpečnostních politik v tomto prostředí. Bezpečnostní politika je sada oprávnění, na které virtuální stroje Javy (JVM) omezují možnosti spuštěných aplikací. Právě možnosti používání bezpečnostních politik byly ve WildFly dosud silně omezeny. Výsledkem práce jsou rozšiřující moduly WildFly, doplňující programové rozhraní WildFly a webovou administrační konzolu WildFly o možnost centrálního nasazování bezpečnostních politik na jednotlivé servery domény WildFly bez potřeby jejich restartu. Součástí výsledku je také záplata samotného jádra WildFly, řešící problém výměny bezpečnostní politiky za běhu JVM., WildFly is a platform for distributed environment which meets specification of Java Enterprise Edition. This thesis deals with possibilities of centralized management of security policies in this environment. Security policy is a set of permissions to which the Java virtual machine (JVM) limits possibilities of running applications. Just possibilities of security policy using was in WildFly so far heavily restricted. The result of the thesis are extensions of WildFly which add possibility of central deployment of security policies to individual servers, without need for restart that server, into program interface of WildFly and into WildFly management console. Part of result is also patch of core of WildFly, which solve problem of exchange security policy at runtime of JVM.

Práce se zabývá tvorbou umělé inteligence pro počítačem řízené prvky a jejich provedení do podoby počítačové hry. V práci jsou dále uvedeny typické postupy při řešení některých problémů rozhodování umělé inteligence a jejich implementace do funkční aplikace., This Bachelor's thesis is focused on artificial intelligence for computer controlled objects, represented by computer game. There are contained typical procedures to handle some behavior problems of intelligent objects and finally their implementation into fully functional application.

Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ., Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.

Tato práce se zabývá porovnáváním jazyků automatů a redukcí automatů používaných při monitorování síťového provozu. Je navrženo několik přístupů pro přibližnou redukci automatů (nezachovávající jazyk) a přístup pro porovnávání jejich jazyků. Redukce jsou založeny na podaproximaci jazyka automatu, kdy dochází k odstraňování stavů nebo na nadaproximaci jazyka, kdy dochází k přidávání nových smyček (a odstranění zbytečných stavů později). Navržené metody pro přibližnou redukci a navržená pravděpodobnostní vzdálenost využívají informaci ze síťového provozu. Jsou poskytnuty formální záruky vzhledem k modelu síťového provozu, který je reprezentován pravděpodobnostním automatem. Metody byly implementovány a jejich vlastnosti byly ověřeny na automatech používaných pro filtrování síťového provozu., The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.

Výkonností testování aplikací nabírá v poslední době na důležitosti během vývoje všeho druhu. Tato práce mapuje základy testování výkonu, které jsou aplikovatelné na libovolné aplikace a následně analýzuje testování výkonu komponent používaných v Messaging systémech a to konkrétně Apache ActiveMQ Artemis a Qpid-Dispatch. Využívané metody testování výkonu je zaměřeno zejména na Apache ActiveMQ Artemis pomocí systému Messaging Performance Tool s názvem Maestro. Práce navrhuje vylepšení této aplikace o rozšíření testování systému Qpid-Dispatch a její možnosti při automatizovaném testování. Řešení je demonstrováno na sérii experimentů s různými topologiemi. Výsledná zpráva závěrem vyhodnocuje navržené rozšíření systému Maestro, zhodnocuje výkon komponenty Qpid-Dispatch a rozvíjí myšlenky pro další rozšíření., Application performance testing has recently become more important during the application development of all kinds. This paper maps the fundamentals of performance testing that are commonly used and it analyzes performance testing of components used in Messaging systems, especially Apache ActiveMQ Artemis and Qpid-Dispatch. However, currently used methods for performance testing of these components are primarily focused only on Apache ActiveMQ Artemis by system Messaging Performance Tool called Maestro. This paper proposes improvements of Messaging Performance Tool to allow proper performance testing of Qpid-Dispatch and its capabilities in automatic testing. The solution is demonstrated on series of experiments with different topologies. The final report evaluates the proposed application, the performance of Qpid-Dispatch component and develops ideas for future works.

Práce se zabývá implementací průběžné integrace pro build systém Copr. Implementace využívá framework Citool a jeho moduly, které se již používají pro průběžnou integraci build systému Koji. Výsledný systém umožňuje automaticky spustit testování pro nový balíček v build systému Copr a otestovat ho v prostředí virtuálního stroje. Práce ukazuje způsob, jakým je možné realizovat průběžnou integraci pro build systém Copr., This thesis deals with implementation of continuous integration for build system Copr. The implementation uses framework Citool and its modules, which are already used for continuous integration of build system Koji. The outcome system can run the tests for the new package from the build system Copr and test it on virtual machine. This thesis shows way how to implement continuous integration for build system Copr.

Cieľom bakalárskej práce je vytvorenie systému na automatizované testovanie GUI desktopových aplikácií, ktorý sa dá jednoducho nasadiť ako testovacie prostredie. Tento systém pozostáva z nástroja, v ktorom je užívateľ schopný vytvárať testovacie skripty, a interpretu, ktorý spúšťa dané testovacie skripty a vyhodnocuje ich. Testovacie skripty užívateľ vytvára pomocou jazyka, ktorý je tiež popísaný v tejto práci. Jednoduché nasadenie systému zabezpečuje použitie kontajnerovej virtualizácie., The aim of this Bachelor thesis is to create a system for automated testing of GUI desktop applications that may be easily used as a test environment. The system consists of, first, an application in which the user is able to create the test scripts, and second, the interpreter that runs and evaluates the relevant test scripts. The user creates the test scripts using a~language that is also described in this thesis. Simple deployment of the system ensures the use of container-based virtualization.

Cloudová řešení získávají na popularitě, spolu s tím však roste jejich složitost. Pro jejich efektivní správu a řízení existují různá řešení. Projekt ManageIQ je jedním z těchto nástrojů. Tato bakalářská práce se zabývá integrací nového poskytovatele cloudové infrastruktury, IBM SoftLayeru, do prostředí správce cloudových řešení ManageIQ. Na tomto příkladě je vysvětleno, jaká rozhraní je třeba použít pro správu poskytovatelů, jak pracovat s cloudovými API a jaké výzvy je třeba řešit při integraci nového poskytovatele. Výsledkem práce je funkční prostředí umožnující snadnou práci v IBM SoftLayeru skrze ManageIQ. To uživateli zprostředkovává sledování a úpravy dostupných zařízení či vytváření a spouštění nových součástí infrastruktury., As cloud computing gains its popularity the complexity of offered services is growing. There exist various different solutions and to manage them effectively is the task for cloud managers. One of them is a project named {ManageIQ}. This thesis aims to describe how to integrate a new provider into this software, what are the required bindings and how to work with the API of the provider. This thesis describes such a process on an IBM SoftLayer provider example. The achieved result enables the user to manage his SoftLayer devices via ManageIQ with ease and also provides him the functionality to provision new appliances.