Bakalářská práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Vliv specifikačních automatů na ověřování modelu

Impact of specification automata to model checking

Vojtěch Rujbr, učo 370641
Anotace

Ověřování modelu pomocí LTL sestává z překladu negace LTL specifikace systému na Büchiho automat, generování produktu tohoto automatu s modelem systému a ověření, zda má produkt prázdný jazyk. Tento proces je typicky náročný na zdroje, především operační paměť. Na efektivitu tohoto procesu má vliv způsob, jakým se překládá LTL specifikace na Büchiho automat. V roce 2003 Sebastiani a Tonetta prezentovali …více

Abstract

An LTL model checking technique consists of translating a negation of an LTL specification for a system into a Büchi automaton, generating a product of this automaton and a model of the system, and checking whether the product has an empty language. This process typically needs a lot of resources, mainly memory. An efficiency of this process can be increased by a way LTL specification is translated …více

Klíčová slova
Model checking linear temporal logic Büchi automaton specification automaton determinism ověřování modelu lineární temporální logika specifikační automat
Zadání práce
Jednou z úspěšných oblastí formální verifikace je ověřování modelu vůči LTL specifikacím založené na využití automatů (automata-based LTL model checking). Prvním krokem algoritmů z této oblasti je překlad specifikační LTL formule na Büchiho automat. Existuje více nástrojů pro tento překlad, které často produkují automaty různých vlastností (např. různý počet stavů, hran, různá míra determinismu). Cílem práce je zjistit, jak ovlivňují vlastnosti vzniklých specifikačních automatů další běh algoritmů pro ověřování modelu. Budou nalezeny (pokud možno reálné) specifikační formule, které běžné nástroje přeloží na různé automaty. Dále bude zkoumán vliv automatů na velikost jejich produktu s (pokud možno reálnými) ověřovanými systémy. Závěrem by mělo být doporučení, jaké vlastnosti mají mít specifikační automaty.
Administrativní informace
Práce zkontrolována:
21. 5. 2013 14:34, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
336 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
17. 6. 2013
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

Dr. Alexandre Duret-Lutz
Autor posudku dosud neidentifikován.

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067.
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.