Diplomová práce

Refined Büchi automata for faster model checking

Bc. Vojtěch Rujbr, učo 370641
Anotace

Ověřování modelu pomocí LTL je formální verifikační metoda, která je typicky velmi náročná na zdroje. V této práci ukážeme, jak je možné zvýšit efektivitu procesu v první fázi ověřování modelu: během překladu LTL specifikací na Büchiho automat. V této práci představíme několik nástrojů, které dokáží ovlivnit proces překladu specifikací na automat pomocí známých informací o modelu. Touto metodou jsme …více

Abstract

An LTL model checking is an advanced formal verification technique typically requiring a lot of resources. In this thesis we show how the efficiency of this process can be improved in the first phase of model checking: translation of an LTL specification into the Büchi automaton. We present tools that influence the translation process or the produced automaton using knowledge about the model. As a …více

Klíčová slova
model checking linear temporal logic Büchi automata specification automata specification refinement label simplification
Zadání práce
The goal of the thesis is to study the influence of LTL (or Büchi automata) specification to efficiency of explicit model checking. More precisely, the specification will be refined with the information about combinations of atomic propositions that cannot appear in the model. The author should present how this information can be used to refine the specificaiton and what is the influence of this refinement to Spin running time.
Administrativní informace
Práce zkontrolována:
8. 1. 2016 10:23, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
4,9 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
15. 2. 2016
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
ITI FI MU

Oponent

prof. RNDr. Luboš Brim, CSc.
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.