|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (referee) ; Šlapal, Josef (referee) ; Švéda, Miroslav (advisor)
Práce představuje model a metody analýzy vlasností komunikace v počítačových sítích. Model dosažitelnosti koncových prvků v IP sítích je vytvořen na základě konfigurace a síťové topologie a umožňuje ukázat, že vabraný koncový uzel je dosažitelný v dané síťové konfiguraci a stavu. Prezentovaná práce se skládá ze dvou částí. První část se věnuje modelování sítí, chování směrovaích protokolů a síťové konfiguraci. V rámci modelu sítě byla vytvořena modifikovaná topologická tabulka (MTT), která slouží pro agregaci síťových stavů určených pro následnou analýzu. Pro analýzu byl použit přístup založený na logickém programování, kdy model sítě je převeden do Datalog popisu a vlastnosti jsou ověřovány kladením dotazů nad logickou databází. Přínosy práce spočívají v definici grafu síťových filtrů, modifikované topologické tabulce, redukce stavového prostoru agrgací síťových stavů, modelů aktivního síťového prvku jako filter-transformace komponenty a metoda pro analýzu dosažitelnosti založena na logickém programování a databázích.
|
|
|
Improving Synthesis of Finite State Controllers for POMDPs Using Belief Space Approximation
Macák, Filip ; Holík, Lukáš (referee) ; Češka, Milan (advisor)
Táto práca sa zameriava na kombináciu dvoch moderných metód syntézy plánovačov pre Markovské procesy s čiastočným pozorovaním (POMDPs), ktoré sú významným modelom pre sekvenčné rozhodovanie s neistotou. Hlavnou úlohou je nájsť plánovač POMDP, ktorý dosahuje čo najlepšiu hodnotu. Keďže hľadanie optimálneho plánovača je nerozhodnuteľné, zameriavame sa na syntézu dobrých konečne stavových kontrolérov (FSCs). V tejto práci integrujeme dve moderné, ortogonálne metódy pre syntézu kontrolérov POMDP, a to metódu založenú na prehľadávaní belief priestoru a induktívnu metódu. Prvá metóda získava FSC z konečného fragmentu takzvaného belief MDP, čo je MDP, ktorý udržiava prehľad o pravdepodobnostiach rovnako pozorovateľných stavov POMDP. Druhá je induktívna vyhľadávacia technika pre množinu FSC s fixnou veľkosťou pamäti. Kľúčovým výsledkom tejto práce je symbiotický algoritmus, ktorý integruje obidva tieto prístupy tak, aby sa každý dokázal zlepšiť z kontrolérov vytvorených tým druhým. Experimentálne výsledky naznačujú významné zlepšenie hodnoty kontrolérov pri značnom znižovaní času syntézy a využitej pamäte.
|
|
|
From textual specification to formal verification
Šimko, Viliam ; Hnětynka, Petr (advisor) ; Gruhn, Volker (referee) ; Steinberger, Josef (referee)
Textual use-cases have been traditionally used at the design stage of the software development process to describe software functionality from the user's perspective. Because use-cases typically rely on natural language, they cannot be directly subject to formal verification. Another important artefact is the domain model, a high-level overview of the most important concepts in the problem space. A domain model is usually not constructed en bloc, yet it undergoes refinement starting from the first prototype elicited from text. This thesis covers two closely related topics - formal verification of use-cases and elicitation of a domain model from text. The former is a method (called FOAM) that features simple user-definable annotations inserted into a use-case to make it suitable for verification. A model-checking tool is employed to verify temporal invariants associated with the annotations while still keeping the use-cases understandable for non-experts. The latter is a method (titled Prediction Framework) that features an in-depth linguistic analysis of text and a sequence of statistical classifiers (log-linear Maximum Entropy models) to predict the domain model.
|
|
|
Verification of Textual Use-Cases
Vinárek, Jiří ; Šimko, Viliam (advisor) ; Hauzar, David (referee)
The aim of this thesis is to create a tool for formal verification of systems specified using textual use- cases. The tool should allow for automated verification of temporal invariants specified in temporal logic (CTL and LTL formulae). The textual specification is transformed to a formal model that is verified using the NuSMV symbolic model-checker. Potential errors are shown to the user in the form of an HTML report. Using this feedback, the user is able to iteratively develop valid textual use-case specifications. The tool's architecture should be focused on reusability of its components and extensibility. Powered by TCPDF (www.tcpdf.org)
|
|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (referee) ; Šlapal, Josef (referee) ; Švéda, Miroslav (advisor)
Práce představuje model a metody analýzy vlasností komunikace v počítačových sítích. Model dosažitelnosti koncových prvků v IP sítích je vytvořen na základě konfigurace a síťové topologie a umožňuje ukázat, že vabraný koncový uzel je dosažitelný v dané síťové konfiguraci a stavu. Prezentovaná práce se skládá ze dvou částí. První část se věnuje modelování sítí, chování směrovaích protokolů a síťové konfiguraci. V rámci modelu sítě byla vytvořena modifikovaná topologická tabulka (MTT), která slouží pro agregaci síťových stavů určených pro následnou analýzu. Pro analýzu byl použit přístup založený na logickém programování, kdy model sítě je převeden do Datalog popisu a vlastnosti jsou ověřovány kladením dotazů nad logickou databází. Přínosy práce spočívají v definici grafu síťových filtrů, modifikované topologické tabulce, redukce stavového prostoru agrgací síťových stavů, modelů aktivního síťového prvku jako filter-transformace komponenty a metoda pro analýzu dosažitelnosti založena na logickém programování a databázích.
|
guest ::
