|
|
Učení se automatů pro rychlou detekci anomálií v síťovém provozu
Hošták, Viliam Samuel ; Matoušek, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Táto práca sa zaoberá rýchlou detekciou sieťových anomálií na základe učenia automatov. Popisuje a porovnáva niekoľko vybraných algoritmov učenia automatov, vrátane ich aplikácie na učenie sieťových charakteristík. Pre takto naučené automaty je navrhnutých niekoľko metód detekcie sieťových anomálií, ktoré umožňujú odhaliť tak sekvenčné, ako aj štatistické anomálie v rámci komunikácie. Za týmto účelom využívajú mechanizmy samotných automatov, ich transformáciu, či štatistickú analýzu. Navrhované metódy detekcie boli implementované a vyhodnotené na prevádzke protokolu IEC 60870-5-104 používaného v industriálnych kontrolných systémoch.
|
|
|
Podnikatelský záměr
Holík, Lukáš ; Smolíková,, Lenka (oponent) ; Heralecký, Tomáš (vedoucí práce)
Cílem diplomové práce je vytvořit podnikatelský plán pro pana Davida Mokrého, majitele kavárny s názvem Blue Queen v Boskovicích, který v blízké době chce rozšířit svoji podnikatelskou činnost o další podnik - Black King. Pomocí četných analýz trhu a analýz vnějšího i vnitřního okolí získám data potřebná k vytvoření projektu na vybudování úspěšné nové kavárny, která by se měla stát nejvyhledávanějším podnikem v okolí.
|
|
|
Kongruence pro stromové automaty
Žufan, Petr ; Janků, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Tento článek pojednává o testování ekvivalence stromových automatů (TA). Přináší nový algoritmus vycházející z algoritmu Bonchiho a Pouse pro slovní automaty. Tento nový algoritmus spojuje bisimulaci s determinizací za běhu. Pomocí optimalizace založené na kongruenčním uzávěru se snaží vyhýbat extrémnímu zvětšování stavového prostoru. Z tohoto hlediska je lepší než jiné metody pro tento problém.
|
|
|
IDE for SCADA Development at CERN
Mareček, Matěj ; Holík, Lukáš (oponent) ; Křivka, Zbyněk (vedoucí práce)
The goal of this master's thesis is to design and implement an IDE (Integrated Development Environment) that makes development for SIMATIC WinCC Open Architecture more effective and secure. This thesis is based on a research made by Eindhoven University of Technology and it meets needs of CERN EN ICE SCD section. The developed IDE is built on top of the Eclipse Platform and it uses Xtext for code parsing, scoping, linking and static code analysis. The IDE also supports a new programming language that allows programmers to easily define templates for WinCC OA configuration files. The interpreter of this new language is able to parse a template and a configuration file and decide whether the configuration file matches the template. The practical result of this thesis is an IDE that supports WinCC OA developers at CERN and performs periodical analysis of CERN code written in Control script Language.
|
|
|
Minimization of Counting Automata
Turcel, Matej ; Vojnar, Tomáš (oponent) ; Holík, Lukáš (vedoucí práce)
This works deals with size reduction of counting automata (CA). Counting automata extend the classical finite automata with bounded counters. This allows efficient handling of e.g. regular expressions with repetition: a{5,10}. In this thesis we discusses the simulation relation in CA, which allows us to reduce their size. We rely on classical simulation in finite automata, which we non-trivially extend to CA. The key difference lies in the necessity to simulate counters as well as states. To this end, we present the novel concept of parameterized simulation relation in CA, and propose methods for computing this relation and using it to reduce the size of a CA. The proposed methods have been implemented and their efficiency experimentally evaluated.
|
|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
The goal of this thesis is to implement and experimentally compare antichain-based algorithms with and without abstraction, which decide the emptiness of alternating finite automata. The author also proposes his own algorithms using abstraction and comes up with a few optimizations of existing abstract algorithms. The thesis introduces the theoretical background of studied algorithms and describes efficient ways to implement data structures which are used by these algorithms. The experimental evaluation over random automata shows that the algorithms without abstraction give us better results in general because they do not perform costly evaluation of closed set intersection and complementation. However, in case of automata with high transition density, the algorithms without abstraction tend to decelerate, while the abstract ones accelerate.
|
|
|
Abstraction of State Languages in Automata Algorithms
Chocholatý, David ; Síč, Juraj (oponent) ; Holík, Lukáš (vedoucí práce)
We explore possibilities of using various abstractions of finite automata languages in optimization of automata algorithms used in automata reasoning. We focus on abstracting languages of states to sets of accepted lengths of word or Parikh images, represented as semi-linear sets, and explore options of using them to optimize automata constructions by pruning states based on abstractions of their languages. We propose several abstractions and work on optimizing their performance. We use two common finite automata problems, synchronous product construction and deciding the emptiness of finite automata intersection, as benchmark problems on which we test our optimizations. Nevertheless, our abstractions are applicable on many other typical automata operations, e.g., complement generation etc. Our experiments show that the proposed optimizations reduce generated state space for both benchmark problems substantially.
|
|
|
Knihovna pro binární rozhodovací diagramy
Janků, Petr ; Hrubý, Martin (oponent) ; Holík, Lukáš (vedoucí práce)
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
|
|
|
Efficient Algorithms for Counting Automata
Mikšaník, David ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Counting automata (CAs) are classical finite automata extended with bounded counters. They still denote the class of regular languages but in a more compact way than finite automata. Since CAs are a recent model, there is a gap in the knowledge of efficient algorithms implementing various operations on the CAs. In this thesis, we mainly focus on an existing subclass of CAs called monadic counting automata (MCAs), i.e., CAs with counting loops on character classes, which are common in practice (e.g., detection of packets in network traffic, log analysis). For this subclass, we efficiently solve the emptiness and inclusion problems. Moreover, we provide two extensions of the class of MCAs (but not beyond the class of CAs) and efficiently solve the emptiness problem for them. MCAs naturally arise from regular expressions that are extended by the counting operator limited only to character classes. Thus our algorithm solving the inclusion problem of MCAs can be used in a new method for solving the inclusion problem of such regular expressions. We experimentally evaluated this method on regular expressions from a wide range of applications and compared it with the naive method. The experiments show that the method using our algorithm is less prone the explode. It also outperforms the naive method if the regular expressions contain counting operators with large bounds. As expected, for the easy cases, the naive method is still faster than the method based on our algorithm.
|
|
|
Optimalizace testování pomocí algoritmů prohledávání prostoru
Starigazda, Michal ; Holík, Lukáš (oponent) ; Letko, Zdeněk (vedoucí práce)
Testování vícevláknových programů je náročný proces kvůli velkému množství možných interakcí mezi vlákny, které je třeba otestovat. Technika vkládání šumu umožňuje zvýšit počet otestovaných proložení (interakcí) konkurenčních vláken generováním šumu. Tato práce optimalizuje techniky prohledávání prostoru v oblasti testování vícevláknových programů, a to s využitím deterministických heuristik použitých při aplikací genetických algoritmů na prostor míst v běhu programu, do kterých je možné umístit šum. V práci je navrženo několik nových heuristik vkládání šumu, které jsou deterministické, narozdíl od většiny současných heuristik pracujících s generátorem náhodných čísel. Motivací odstranění náhodnosti je informovanější prohledávání a získávání optimálnějších výsledků pomoci zvýšení stability výsledku poskytovaných novými heuristikami. Součástí práce je i základní sada testovacích programů, která bude použita k vyhodnocení výsledků nových heuristik vkládání šumu.
|
host ::
RSS.