|
|
Dynamické analyzátory pro platformu SearchBestie
Janoušek, Martin ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato diplomová práce se zabývá návrhem a implementací dynamického analyzátoru kontraktů s parametry. V první části práce je představena problematika testování paralelních programů, včetně metod testování a chyb, které se mohou v těchto programech nacházet. Podrobněji se zabývá metodou dynamické analýzy a věnuje se konkrétním dynamickým analyzátorům, jako jsou FastTrack nebo analyzátor kontraktů. Ve druhé části práce je popsán návrh a implementace dynamického analyzátoru kontraktů pro framework RoadRunner a platformu Searchbestie .
|
|
|
Support for Dynamic Config Reload Inside Rsyslog
Lakatos, Attila ; Češka, Milan (oponent) ; Rogalewicz, Adam (vedoucí práce)
Logs are one of the most valuable assets when it comes to IT system management and mon- itoring. As they record every action that took place on a machine, logs provide the insight system administrators need to spot issues that might impact performance, compliance, and security. For this reason, the rsyslog software utility can be used as it offers the ability to accept inputs from a wide variety of sources, transform them, and output the results to diverse destinations by a set of rules. One shortcoming the software currently has is that it needs to be restarted in order to modify the rule set. The author of this master's thesis points out what types of problems a user might encounter during this period of time, such as messages entering the system are lost, TCP/UDP based connections are disturbed, even if no changes are made. The goal of this thesis is to design and implement an option, which allows users to dynamically reload configuration for core components without the need of a full restart. The improvements aim to address problems raised by the research, as well as increase performance by reusing already existing resources.
|
|
|
Bounded model checking v nástroji Java PathFinder
Dudka, Vendula ; Češka, Milan (oponent) ; Křena, Bohuslav (vedoucí práce)
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce Java, a proto pro verifikační metodu byl zvolen model checker Java Pathfinder, který je určen pro Java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.
|
|
|
Konstrukce efektivních automatů pro rozpoznávání regulárních výrazů v HW
Frejlach, Jakub ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Motivací této bakalářské práce je užití rozpoznávání regulárních výrazů v aplikačních doménách, kde je vyžadováno rychlé rozpoznávání jako například v hloubkové kontrole paketů. Během akcelerace jsou regulární výrazy ve formě nedeterministických konečných automatů syntetizovány na FPGA. Ačkoliv hardwarová akcelerace řeší rychlostní problémy, tak trpí zvýšenou spotřebou FPGA součástek, konkrétně LUT. Tato práce se zabývá návrhem, implementací a experimentálním vyhodnocením heuristické metody pro aproximaci konečných automatů pro rozpoznávání regulárních výrazů v hardware. Účelem této aproximace je snížení spotřeby LUT součástek při syntéze na FPGA. Princip redukční metody je založen na přidávání nových přechodů, čímž je zajištěna tvorba menšího počtu znakových tříd a je tak dosaženo zredukování spotřeby LUT při implementaci přechodů. Zavedená nepřesnost je minimalizována modifikací pouze méně významných částí automatu. Navržená metoda i s testovacím prostředím je implementována v nástroji TOFA. Technika byla vyhodnocena na syntetických i reálných datech. Výsledky experimentů ukázaly, že přechodová aproximace zvláště dobře funguje na automatech, kde se vyskytuje velký počet znakových tříd.
|
|
|
Nové modely pro automatickou detekci degradace výkonu
Stupinský, Šimon ; Češka, Milan (oponent) ; Rogalewicz, Adam (vedoucí práce)
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.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This work discusses adversarial attacks to image classifier neural network models. Our goal is to summarize and demonstrate adversarial methods to show that they pose a serious issue in machine learning. The important contribution of this work is the implementation of a tool for training a robust model against adversarial examples. Our approach is to minimize maximization the loss function of the target model. Related work and our own experiments leads us to use Projected gradient descent as a target attack, therefore, we train against data generated by Projected gradient descent. As a result using the framework, we can achieve accuracy more than 90% against sophisticated adversarial attacks.
|
|
|
Ověřování temporálních vlastností konečných běhů programů
Sečkařová, Petra ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Temporální vlastnosti programů jsou používány ke specifikaci korektního průběhu jejich vykonávání. Jedním z nejčastějších způsobů formálního popisu těchto vlastností je lineární temporální logika - LTL , případně její varianty. Tato práce se zabývá návrhem a implementací nástroje pro automatizované ověřování temporálních vlastností běhů programů specifikovaných pomocí LTL minulého času (past-time LTL). Výsledný program na základě dané specifikace vygeneruje statickou knihovnu, která dokáže spolehlivě ověřit, zda jsou její formule v každém okamžiku běhu kontrolovaného programu splněny, a případné neočekávané nebo nesprávné chování hlásí společně s podrobnou zprávou o okolnostech tohoto chybového stavu, která má napomáhat k nalezení chyby v konkrétním místě kódu.
|
|
|
Využití přibližné ekvivalence při návrhu přibližných obvodů
Matyáš, Jiří ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Tato práce je zaměřena na využití formálně verifikačních technik pro návrh funkčních aproximací kombinačních obvodů. Jsou zde důkladně prostudovány existující formální přístupy pro zkoumání přibližné ekvivalence a jejich použití při vývoji aproximovaných obvodů. V rámci této práce je navržena nová metoda, která integruje vybrané formální techniky do Kartézského genetického programování. Klíčovým bodem nového přístupu je využití prohledávací strategie, která vede evoluci směrem k řešením, která lze rychleji verifikovat. Navržený algoritmus byl implementován v rámci syntézního nástroje ABC. Jeho výkonnost byla otestována na vývoji funkčních aproximací násobiček a sčítaček s šířkami vstupních operandů 32, respektive 128 bitů. Dosažené výsledky ukazují výjimečnou škálovatelnost navržené metody.
|
|
|
Nástroj pro generování obsahu databáze pro účely testování softwaru
Želiar, Dušan ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Cieľom bakalárskej práce je vytvoriť nástroj na generovanie obsahu databázy pre účely testovania. Podstatou nástroja je vytvorenie náhodných dát, ktoré spĺňajú zadané obmedzenia. Obmedzenia popisujú štrukturálne väzby v relačnej databáze a sémantické závislosti medzi hodnotami jednotlivých stĺpcov tabuliek. Výsledkom tejto práce je nástroj, ktorý podľa definovaných obmedzení postupne generuje a vkladá dáta do databázy. Záver práce obsahuje demonštráciu funkcionality na databáze reálneho charakteru.
|
|
|
Advanced Methods for Synthesis of Probabilistic Programs
Stupinský, Šimon ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce)
Probabilistic programs play a crucial role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. PAYNT is a tool for the automatic synthesis of probabilistic programs satisfying the given specifications. In this thesis, we extend this tool primarily to support optimal synthesis and synthesis for multi-property specifications. Further, we have proposed and implemented a new method that can efficiently synthesise continuous parameters affecting the transition probabilities alongside the synthesis of a program topology, i.e., support of both topology and parameter synthesis at the same time. We demonstrate the usefulness and performance of PAYNT on a wide range of real-world case studies from various application domains. For challenging synthesis problems, PAYNT can significantly decrease the run-time from days to minutes while ensuring the completeness of the synthesis process.
|
host ::
RSS.