Diplomová práce

Verifikační manažer pro explicitní ověřování modelu

Verification manager for explicit model checking

Bc. Václav Rosecký
Anotace

Předmětem této práce je implementace a experimentální vyhodnocení verifikačního manažera pro ověřování modelů, což je nástroj pro efektivní spouštění verifikačních technik v distribuovaném prostředí. Verifikační proces je řízen na základě uživatelem dodané obecné verifikační strategie.

Abstract

The subject of the thesis is implementation and experimental evaluation of verification manager for model checking, which is a tool for efficient execution of verification techniques in distributed environment. The verification process is driven by general verification strategy.

Klíčová slova
verifikační manažer verification manager ověřování modelů model checking detekce chyb error detection DiVinE LTL
Zadání práce
Cílem práce je vytvořit nástroj, který bude koordinovat spouštění verifikačních technik ("verifikační manažer"). Manažer bude implementován v Javě jako nádstavba nad algoritmy nástroje DiVinE pro explicitní ověřování modelů. Výsledný nástro by měl být schopen:
  • Pracovat v distribuovaném prostředí.
  • Spouštět více verifikačních algoritmů současně a vhodně reagovat na výstupy (úspěšné/neuspěšné ukončení verifikace).
  • Vyhodnocovat několik instancí verifikačního problému současně.
  • Pracovat na základě obecné verifikační "strategie" dodané uživatelem.
Součástí práce bude vyhodnocení nástroje pomocí příkladů z databáze příkladů BEEM.
Administrativní informace
Práce zkontrolována:
12. 1. 2010 08:44, doc. Mgr. Radek Pelánek, Ph.D., učo 4297
Plný text práce
2,7 MB / soubor PDF
Jazyk práce
čeština čeština
Termín obhajoby
8. 2. 2010
Práce byla úspěšně obhájena

Vedoucí

doc. Mgr. Radek Pelánek, Ph.D., učo 4297
KSUZD FI MU

Oponent

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
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
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Václav Rosecký FI N-AP AP i2qqj/7
Rosecký, V.
9. 1. 2010
Složky
Soubory
Anotace anglicky annotation_english.txt
Rosecký, V.
9. 1. 2010
Anotace česky annotation.txt
Rosecký, V.
9. 1. 2010
dp.tar.bz2
Rosecký, V.
10. 1. 2010
Klíčová slova keywords.txt
Rosecký, V.
9. 1. 2010
posudek_oponenta.pdf
Barnat, J.
26. 1. 2010
Text práce emma.pdf
Rosecký, V.
10. 1. 2010

  • 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.