|
|
Induktivní syntéza konečně stavových kontrolérů pro decentralizované POMDP
Hranička, Vojtěch ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Markovovy rozhodovací procesy s částečným pozorováním~(POMDP) jsou významným stochastickým modelem pro sekvenční rozhodování s nejistotou. Decentralizované POMDP~(Dec-POMDP) tento model rozšiřují o možnost práce s více agenty. Tato práce se zaměřuje na rozšíření metody induktivní syntézy kontrolérů pro POMDP, tak aby podporovala práci s Dec-POMDP. Hlavním cílem syntézy je nalézt takové kontroléry pro každého z agentů, aby jejich společné chování nejlépe splňovalo požadované specifikace. V této práci se zaměřuji na strategie, které jsou reprezentovány pomocí konečně stavových kontrolérů~(FSC). Experimentální výsledky ukazují, že použití této metody pro návrh kontrolérů dosahuje srovnatelných výsledků se state-of-the-art přístupy. Navíc tento přístup jako první umožňuje práci v nekonečném horizontu bez použití discount faktoru. Díky tomu je tato metoda vhodnější pro řešení problémů, kde je důležité rozhodnutí provedeno až v pozdějším horizontu.
|
|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (oponent) ; Šlapal, Josef (oponent) ; Švéda, Miroslav (vedoucí práce)
The objective of the research is to model and analyze the effects of dynamic routing protocols. The thesis addresses the analysis of service reachability, configurations, routing and security filters on dynamic networks in the event of device or link failures. The research contains two main sections, namely, modeling and analysis. First section consists of modeling of network topology, protocol behaviors, device configurations and filters. In the modeling, graph algorithms, routing redistribution theory, relational algebra and temporal logics were used. For the analysis of reachability, a modified topology table was introduced. This is a unique centralized table for a given network and invariant for network states. For the analysis of configurations, a constraint-based analysis was developed by using XSD Prolog. Routing and redistribution were analyzed by using routing information bases and for analyzing the filtering rules, a SAT-based decision procedure was incorporated. A part of the analysis was integrated to a simulation tool at OMNeT++ environment. There are several innovations introduced in this thesis. Filtering network graph, modified topology table, general state to reduce the state space, modeling devices as filtering nodes and constraint-based analysis are the key innovations. Abstract network graph, forwarding device model and redistribution with routing information are extensions of the existing research. Finally, it can be concluded that this thesis discusses novel approaches, modeling methods and analysis techniques in the area of dynamic networks. Integration of these methods into a simulation tool will be a very demanding product for the network designers and the administrators.
|
|
|
From textual specification to formal verification
Šimko, Viliam ; Hnětynka, Petr (vedoucí práce) ; Gruhn, Volker (oponent) ; Steinberger, Josef (oponent)
Běžný způsob popisu funkčních požadavků při vývoji softwaru je tvorba textových případů použití (use-cases). Jejich úlohou v úvodních fázích projektu je zachytit formou přirozeného jazyka způsob fungování systému z pohledu koncového uživatele. Protože jde o text psaný v přirozeném jazyce, není možné správnost textových případů použití přímo formálně ověřovat. Obdobně významným artefaktem při vývoji software je doménový model. Jde o popis nejdůležitějších konceptů a vztahů, které jsou pro vyvíjenou aplikaci důležité. Tvorba doménového modelu běžně probíhá iterativně od prvního prototypu z textu až po výsledný formální model. Tato práce se zabývá dvěma souvisejícími tématy - formální ověřování případů použití a odvozování doménového modelu z textu. První část je věnovaná metodě FOAM, která umožňuje pomocí jednoduchých anotací vložených do textu případů použití formálně ověřovat jejich správnost (model-checking). Anotace umožňují zachytit větvení kroků v případech použití a uživatel má možnost vyjádřit časové závislosti mezi různými částmi specifikace, zároveň je však zachovaná srozumitelnost původního textu. Druhá část práce popisuje tzv. Prediction Framework, který pomocí lingvistické analýzy textu a statistických klasifikátorů (log-linear Maximum Entropy models) umožňuje predikování doménového model z textu.
|
|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (oponent) ; Šlapal, Josef (oponent) ; Švéda, Miroslav (vedoucí práce)
The objective of the research is to model and analyze the effects of dynamic routing protocols. The thesis addresses the analysis of service reachability, configurations, routing and security filters on dynamic networks in the event of device or link failures. The research contains two main sections, namely, modeling and analysis. First section consists of modeling of network topology, protocol behaviors, device configurations and filters. In the modeling, graph algorithms, routing redistribution theory, relational algebra and temporal logics were used. For the analysis of reachability, a modified topology table was introduced. This is a unique centralized table for a given network and invariant for network states. For the analysis of configurations, a constraint-based analysis was developed by using XSD Prolog. Routing and redistribution were analyzed by using routing information bases and for analyzing the filtering rules, a SAT-based decision procedure was incorporated. A part of the analysis was integrated to a simulation tool at OMNeT++ environment. There are several innovations introduced in this thesis. Filtering network graph, modified topology table, general state to reduce the state space, modeling devices as filtering nodes and constraint-based analysis are the key innovations. Abstract network graph, forwarding device model and redistribution with routing information are extensions of the existing research. Finally, it can be concluded that this thesis discusses novel approaches, modeling methods and analysis techniques in the area of dynamic networks. Integration of these methods into a simulation tool will be a very demanding product for the network designers and the administrators.
|
host ::
RSS.