|
|
Advanced Methods for Synthesis of Probabilistic Programs
Stupinský, Šimon ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce)
Probabilistic programs play a crucial role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. PAYNT is a tool for the automatic synthesis of probabilistic programs satisfying the given specifications. In this thesis, we extend this tool primarily to support optimal synthesis and synthesis for multi-property specifications. Further, we have proposed and implemented a new method that can efficiently synthesise continuous parameters affecting the transition probabilities alongside the synthesis of a program topology, i.e., support of both topology and parameter synthesis at the same time. We demonstrate the usefulness and performance of PAYNT on a wide range of real-world case studies from various application domains. For challenging synthesis problems, PAYNT can significantly decrease the run-time from days to minutes while ensuring the completeness of the synthesis process.
|
|
|
Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji.
|
|
|
Formal verification of RISC-V processor with Questa PropCheck
Javor, Adrián ; Fujcik, Lukáš (oponent) ; Dvořák, Vojtěch (vedoucí práce)
The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.
|
|
|
Model checking nekonečně stavových systémů založený na inferenci jazyků
Rozehnal, Pavel ; Křena, Bohuslav (oponent) ; Vojnar, Tomáš (vedoucí práce)
Regulární model checking je metoda pro verifikaci nekonečně stavových systémů. Je založena na kódování jejich konfigurace jako slov nad konečnou abecedou, množiny konfigurací jako konečného automatu a přechodů jako konečných transducerů. Je zde představen nový přístup k regulárnímu model checkingu založený na odvozování regulárních jazyků. Metoda je založena na prozkoumávání nekonečně stavového systému, jehož chování může být modelováno použitím transducerů, které zachovávají délku řetězců a jejich aplikací je možné získat všechny dosažitelné konfigurace systému. Naše metoda regulárního model checkingu je založena na odvozování regulárních jazyků pomocí algoritmu Angluin, který je použit pro nalezení vhodného invariantu (nadaproximace), který je schopen zodpovedět otázku zachování či porušení nějaké vlastnosti. Je zde také uveden úvod do teorie konečných automatů, model checkingu, SAT problémů a popis Angluinova a Biermanova algoritmu pro učení konečných automatů.
|
|
|
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
|
|
|
Vliv ABS na chování vozidla
Zich, Jakub ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Bakalářská práce se zabývá systémem ABS (Anti-lock braking system) a jeho vlivem na délku brzdné dráhy vozidla. Práce obsahuje rešerši k tomuto problému, přehled vhodných modelovacích prostředků, návrh řešení, jeho implementaci v modelovacím nástroji UPPAAL a testy prováděné s modelem. Testy zkoumají průběh vývoje základních veličin spojených s brzděním (rychlost, brzdná dráha, skluz, úhlová rychlost, koeficient tření) v simulacích nouzového brzdění s použitím systému ABS a bez něj, a výsledky porovnávají. Taktéž ověřují pravděpodobnost, že vozidlo zastaví v různých podmínkách za danou vzdálenost. V neposlední řadě umí model simulovat poruchu brzd či brzdových čidel a výsledky těchto simulací je možné porovnávat se simulacemi bez poruchy.
|
|
|
Improving Synthesis of Finite State Controllers for POMDPs Using Belief Space Approximation
Macák, Filip ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce)
This work focuses on combining two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller that achieves a total expected reward objective. As finding optimal controllers is undecidable, we concentrate on synthesising good finite-state controllers (FSCs). We do so by tightly integrating two modern, orthogonal methods for POMDP controller synthesis: a belief-based and an inductive approach. The former method obtains an FSC from a finite fragment of the so-called belief MDP, an MDP that keeps track of the probabilities of equally observable POMDP states. The latter is an inductive search technique over a set of FSCs with a fixed memory size. The key result of this work is a symbiotic anytime algorithm that tightly integrates both approaches such that each profits from the controllers constructed by the other. Experimental results indicate a substantial improvement in the value of the controllers while significantly reducing the synthesis time and memory footprint.
|
|
|
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.
|
|
|
GIMPLE Model Checker
Krč-Jediný, Ondrej ; Šerý, Ondřej (vedoucí práce) ; Hauzar, David (oponent)
Název práce: GIMPLE Model Checker Autor: Ondrej Krč-Jediný Katedra (ústav): Katedra distribuovaných a spolehlivých systémů Vedoucí diplomové práce: RNDr. Ondřej Šerý Ph.D. e-mail vedoucího: Ondrej.Sery@mff.cuni.cz Abstrakt: Cieľom práce je implementácia základných prvkov explicit-state model checkeru pre jazyk C - pokročilého nástroja na hľadanie chýb v programoch. Tento nástroj prehľadáva všetky možné cesty, ktorými môže byť program vykonávaný a zároveň vyskúša všetky možné kombinácie prekladania vlákien. Nástroj je založený na GIMPLE - výstupe front-endu kompilátora GCC, ktorý berie za svoj vstupný jazyk. Práca využíva predchádzajúcu prácu 'Memory representa- tion for GIMPLE Model Checker', ktorá implementuje prácu s pamäťou pre tento nástroj. Tým, že je nástroj vychádza z GIMPLE, umožňuje overovanie systémov priamo v jazyku C, naviac je ľahko rozšíriteľný na iné jazyky podporované GCC. 1
|
|
|
State Space Symmetry Reduction for TBP Analysis
Černý, Ondřej ; Šerý, Ondřej (vedoucí práce) ; Poch, Tomáš (oponent)
Threaded Behavior Protocols (TBP) je specifikační jazyk pro modelování chování softwarových komponent. Tato práce se zaměřuje na analýzu TBP specifikací v rámci prostředí, která obsahují neomezené množšví replikovaných vláken. Takové specifikace spolu s modely možných prostředí způsobí nekonečnost stavového prostoru analýzy, který obsahuje velké množství symetrií, způsobených replikací vláken. V práci je navžena technika analýzy takových modelů, která redukuje symetrie s použitím abstrakce zvané Symbolic Counter Abstraction. Pro její použití je však nutné převést vlastnosti modelu na problém dosažitelnosti stavů vláken. Navrhovaná technika je bezpečná ve smyslu odhalení všech chyb v modelu. Na druhou stranu může způsobovat tzv. spurious erros, tj. chyby které neodpovídají skutečným chybám v modelu. Tyto chyby jsou v práci dobře identifikovány a dále jsou nastíněny způsoby jejich redukce. Práce navíc může představovat malý krok směrem k podpoře dynamického vytváření vláken v TBP specifikacích.
|
host ::
RSS.