|
|
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.
|
|
|
Analýza plánovatelnosti úloh reálného času s ohledem na nejistotu
Čus, Samuel ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této bakalářské práce je seznámení se se systémy pracujícími v reálném čase, nejistotami a plánovacími mechanismy, souvisejícími s těmito systémy, statistickým ověřováním modelů, dále je to návrh a implementace přístupu k analýze plánovatelnosti s ohledem na nejistoty, vytvoření vhodných sad úloh reálného času a ověření jejich plánovatelnosti. Zaměřil jsem se na nejistoty způsobené přerušením systému a nedeterministickými parametry úloh. Zadaný problém jsem řešil vytvořením sad úloh, zavedením nejistot do systému a analýzou plánovatelnosti úloh. Modelování systému a jeho analýza bylo provedeno v nástroji UPPAAL SMC pro porovnaní také v nástroji Cheddar u vybraných sad úloh.
|
|
|
Using inheritance dependencies to accelerate abstraction-based synthesis of finite-state controllers for POMDPs.
Shevchenko, Aleksandr ; Macák, Filip (oponent) ; Češka, Milan (vedoucí práce)
Partially observable Markov decision process is an important model for autonomous planning used in many areas, such as robotics and biology. This work focuses on the Abstraction-Refinement framework for the inductive synthesis of finite-state controllers (FSCs) for POMDPs. The classic version of AR requires model checking of a quotient MDP for an entire set of compatible choices of the subfamily in each iteration. We propose an algorithm that uses inheritance dependencies to reduce the size of the quotient MDP’s mask and accelerate model checking for subfamilies of FSCs. We also introduce a smart version of this algorithm, which preserves all its advantages and reduces its weaknesses. During the experiments, it turned out that our approach also affects the operation of other parts of the synthesis, e.g. model building. Depending on the POMDP model, we observe both speedups and slowdowns in comparison to AR. On average, our approach speeds up the overall synthesis time by 1.2 times, and in some cases up to the factor 10.
|
|
|
HyperLTL Model Checking
Alexaj, Ondrej ; Strejček, Jan (oponent) ; Lengál, Ondřej (vedoucí práce)
HyperLTL model checking is an approach to verifying a system against a given hyperproperty, which is able to relate multiple executions of a system. The algorithmic approach based on automata which relies on standard -automata operations is well established. The aim of this work is to outperform the complete state-of-the-art HyperLTL model checker AutoHyper by employing more efficient partial automata operations, in particular complementation and inclusion. The implementation of HyperLTL model checking in a novel modular-based complementation tool Kofola resulted in a significant enhancement in performance compared to the reference tool. Finally, our approach to language inclusion checking shows a notable improvement in terms of the generated state space. As a commonly used automata operation, it could potentially contribute to the advancement of other areas of verification.
|
|
|
Fault relevance diagnostics of the PMSM under the inter-turn short circuit fault
Zezula, Lukáš ; Václavek, Pavel (oponent) ; Blaha, Petr (vedoucí práce)
This thesis describes the mathematical modeling of a permanent magnet synchronous motor under a stator winding's inter-turn short circuit fault, the discretization of obtained model, and the model-based fault relevance diagnostics. A description of a shorted machine is formed in the stator variables assuming the series-parallel winding connection and transformed into the rotor reference frame using extended Clarke's and Park's transformation matrix. A discrete-time equivalent of the designed model is formed based on the linear time-varying systems approach, considering the electrical angular velocity time-varying parameter with a defined integral. The discrete-time model is transformed into the stator reference frame to maximize the persistence of input signals. The fault relevance diagnostics are then realized based on the recursive parametric estimation of the discrete-time model. In addition, one chapter is dedicated to the control system description since the short circuits may affect state variables differently depending on the control system architecture and tuning. The experimental validation of the presented ideas follows at the end of each chapter.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
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.
|
|
|
Translation of LTL with Bounded Repetition to Automata with Counters
Slezáková, Alexandra ; Smrčka, Aleš (oponent) ; Holík, Lukáš (vedoucí práce)
This work solves translation of LTL with bounded repetition (temporal operators that have limited validity for a certain number of steps) to automaton with counters. Using classical methods, the automaton representation of such formulas is large, because the size of automaton may be exponential to the upper limit of the bounded repetition. We present a construction that creates the automaton independent from repetition. The work represents a solution to the problem using the Büchi automaton with counters. The counters ensure that similar states and transitions are not created, which leads to a reduction in the size of the automaton. Our method is implemented and experimentally verified. We reduce the number of states of the automaton for formulas with large bound of operators several times in comparison to classical methods.
|
|
|
Security of Contactless Smart Card Protocols
Henzl, Martin ; Rosa, Tomáš (oponent) ; Staudek, Jan (oponent) ; Hanáček, Petr (vedoucí práce)
This thesis analyses contactless smart card protocol threats and presents a method of semi-automated vulnerability finding in such protocols using model checking. Designing and implementing secure applications is difficult even when secure hardware is used. High level application specifications may lead to different implementations. It is important to use the smart card correctly, inappropriate protocol implementation may introduce a vulnerability, even if the protocol is secure by itself. The goal of this thesis is to provide a method that can be used by protocol developers to create a model of arbitrary smart card, with focus on contactless smart cards, to create a model of the protocol, and to use model checking to find attacks in this model. The attack can be then executed and if not successful, the model is refined for another model checker run. The AVANTSSAR platform was used for the formal verification, models are written in the ASLan++ language. Examples are provided to demonstrate usability of the proposed method. This method was used to find a weakness of Mifare DESFire contactless smart card. This thesis also deals with threats not possible to cover by the proposed method, such as relay attacks.
|
|
|
Generování modelů pro testy ze zdrojových kódů
Kraut, Daniel ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
ílem této diplomové práce je navrhnout a implementovat nástroj pro automatické generování cest ze zdrojových kódů. V rámci práce byla nastudována problematika testování založeného na modelech a navrženo možné řešení automatického generátoru, dle kritérií pokrytí definovaných nad modelem CFG. Stěžejním bodem diplomové práce je návrh a popisuje implementaci nástroje. Nástroj podporuje množství kritérií pokrytí, které umožňují uživateli navrhovaného nástroje zaměřit se na konkrétní aspekt zkoumaného systému, který chce pokrýt testy. Navíc je nástroj přizpůsoben pro další požadavky na velikost generované testovací sady, reflektující reálné požadavky s praktickým využitím. Generátor byl implementován v jazyce C++ a webové rozhraní k němu v jazyce Python, které zároveň slouží pro integraci do platformy Testos.
|
host ::
RSS.