|
|
Dynamic Analyzers for SearchBestie Platform
Janoušek, Martin ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
This master thesis deals with the design and implementation of dynamic analyzer of parametrized contracts . In the first part of the thesis , the problematics of testing of parallel programs are discussed and issues when dealing with parallelism are described . Further , methods how to reveal concurrency bugs via dynamic analysis are described , in particular FastTrack and Contract validator. The second part of the thesis proposes an extension for RoadRunner framework and SearchBestie platform for contract validator with parameters.
|
|
|
Support for Dynamic Config Reload Inside Rsyslog
Lakatos, Attila ; Češka, Milan (referee) ; Rogalewicz, Adam (advisor)
Logy sú jedným z najcennejších aktív, pokiaľ ide o správu IT systému a monitoring. Keďže zaznamenávajú každú činnosť, ktorá sa uskutočnila na stroji, logy poskytujú prehľad správ- covi systému aby vedel zistiť pôvod problémov, ktoré môžu ovplyvniť výkon, súlad a bezpečnosť. Z tohto dôvodu je možné softvérový nástroj rsyslog použiť, keďže ponúka možnosť prijímať vstupy zo širokej škály zdrojov, transformovať ich a odosielať výsledky rôznym destináciám na základe súboru pravidiel. Jedným z nedostatkov tohto softvéru v súčasnosti je to, že ho je potrebné reštartovať, aby akceptoval aktualizované zmeny v pravidlách. Autor tejto diplomovej práce poukazuje na to, s akými typmi problémov sa môže stretnúť užívateľ počas reštartu nástroja. Medzi najkritickejšie patria strata správ vstupujúcich do systému a narušenie TCP/UDP spojenia, aj keď neboli vykonané žiadne zmeny v pravidlách. Cieľom diplomovej práce je navrhnúť a implementovať riešenie, ktoré umožňuje používateľom dynamicky znovu načítať konfiguráciu základných komponentov bez potreby úplného reštartu. Navrhované zmeny sú zamerané aj na riešenie problémov, ktoré boli odhalené počas vývoja ako aj na zvýšenie výkonu opätovným použitím už exis- tujúcich zdrojov.
|
|
|
Bounded Model Checking Using Java PathFinder
Dudka, Vendula ; Češka, Milan (referee) ; Křena, Bohuslav (advisor)
This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.
|
|
|
Construction of Effective Automata for Regex Matching in HW
Frejlach, Jakub ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
This thesis is motivated by the application of REs in domains requiring fast matching such has deep packet inspections. To ensure sufficient speed a HW acceleration is typically employed. During the acceleration, REs are in the form of NFA synthesized on FPGA. Although HW acceleration solves the speed problems, it suffers from increased consumption of the FPGA components, specifically LUT. The goal of this thesis is to design, implement and experimentally evaluate heuristic method for approximation of FA in context of HW accelerated RE matching. The purpose of this approximation is to lower consumption of LUT components during FPGA synthesis. The key idea of the method is to add some transitions allowing to construct a smaller number of character classes and thus to reduce the number of LUT implementing the transition relation while reducing the error by modifying only less significant parts of FA. Proposed method together with evaluation pipeline is implemented in TOFA tool. Technique was evaluated on both synthetic and real data. Results of experiments shows, that transitional approximation works especially well on automatas with large number of equivalence character classes.
|
|
|
New Models for Automatic Detection of Performance Degradation
Stupinský, Šimon ; Češka, Milan (referee) ; Rogalewicz, Adam (advisor)
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.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
Tato práce pojednává o kontradiktorních útocích na klasifikační modely neuronových sítí. Naším cílem je shrnout a demonstrovat kontradiktorní metody a ukázat, že představují vážný problém v strojovém učení. Důležitým přínosem této práce je implementace nástroje pro trénink robustního modelu na základě kontradiktorních příkladů. Náš přístup spočívá v minimalizaci maximalizace chybové funkce cílového modelu. Související práce a naše vlastní experimenty nás vedou k použití Projektovaného gradientního sestupu jako cílového útoku, proto trénujeme proti datům generovaným Projektovaným gradientním sestupem. Výsledkem použití nástroje je, že můžeme dosáhnout přesnosti více než 90% proti sofistikovaným nepřátelským útokům.
|
|
|
Checking of Temporal Properties of Finite Traces of Programs
Sečkařová, Petra ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.
|
|
|
Employing Approximate Equivalence for Design of Approximate Circuits
Matyáš, Jiří ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
This thesis is concerned with the utilization of formal verification techniques in the design of the functional approximations of combinational circuits. We thoroughly study the existing formal approaches for the approximate equivalence checking and their utilization in the approximate circuit development. We present a new method that integrates the formal techniques into the Cartesian Genetic Programming. The key idea of our approach is to employ a new search strategy that drives the evolution towards promptly verifiable candidate solutions. The proposed method was implemented within ABC synthesis tool. Various parameters of the search strategy were examined and the algorithm's performance was evaluated on the functional approximations of multipliers and adders with operand widths up to 32 and 128 bits respectively. Achieved results show an unprecedented scalability of our approach.
|
|
|
A Tool for Database Content Analysis for Testing Purposes
Želiar, Dušan ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
The aim of this bachelor's thesis is to create a tool for generating database content for testing purposes. The main function of the generator is to create random data which meets defined constraints. Constraints describe structural relationships in a database as well as semantic dependencies among columns in tables. The result of the thesis is a tool which generates test and inserts data into database based on defined constraints. The last part of the thesis contains demonstration of the functionality on a real database.
|
|
|
Advanced Methods for Synthesis of Probabilistic Programs
Stupinský, Šimon ; Holík, Lukáš (referee) ; Češka, Milan (advisor)
Pravdepodobnostné programy zohrávajú rozhodujúcu úlohu v rôznych technických doménach, ako napríklad počítačové siete, vstavané systémy, stratégie riadenia spotreby energie alebo softvérové produčkné linky. PAYNT je nástroj na automatizovanú syntézu pravdepodobnostných programov vyhovujúcich zadaným špecifikáciam. V tejto práci rozširujeme tento nástroj predovšetkým o podporu optimálnej syntézy a syntézy viacerých špecifikácií. Ďalej sme navrhli a implementovali novú metódu, ktorá dokáže efektívne syntetizovať parametre so spojitým definičným oborom ovplyvňujúce pravdepodobnostné prechody popri syntéze topológie programov, t.j., podporu pre syntézu topológie aj parametrov súčasne. Demonštrujeme užitočnosť a výkonnosť nástroja PAYNT na širokej škále prípadových štúdií z rôznych aplikačných domén ktoré majú uplatnenie v reálnom svete. Pri náročných problémoch syntézy môže PAYNT výrazne znížiť dobu behu až z dní na minúty a zároveň zaistiť úplnosť procesu syntézy.
|
guest ::
