Bakalářská práce

Post-mortem analýza stavového prostoru

Post mortem analysis of state space

Jan Kriho
Anotace

Cílem BC práce je doplnit verifikační nástroj DiVinE 2.x o možnost exportu při verifikaci vypočteného stavového prostoru do souboru a jeho předzpracování pro případnou budoucí post-mortem analýzu, např. extrakci jiného v době ukončení programu spočítaného protipříkladu.

Abstract

The goal of the thesis is to add feature to export of computed state-space to the file and prepare it for post-mortem analysis, eg. extraction of another counterexample.

Klíčová slova
DiVinE model checking verifikace verification state explosion
Zadání práce
Cílem BC práce je doplnit verifikační nástroj DiVinE 2.x o možnost exportu při verifikaci vypočteného stavového prostoru do souboru a jeho předzpracování pro případnou budoucí post mortem analýzu, např. extrakci jiného v době ukončení programu spočítaného protipříkladu.
Administrativní informace
Práce zkontrolována:
24. 5. 2011 14:36, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
377,1 KB / soubor PDF
Přílohy (1)
Jazyk práce
čeština čeština
Termín obhajoby
24. 6. 2011
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
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 Jan Kriho FI B-IN PDS n3vss/7
Kriho, J.
23. 5. 2011
Složky
Soubory
Anotace anglicky annotation_english.txt
Kriho, J.
23. 5. 2011
Anotace česky annotation.txt
Kriho, J.
23. 5. 2011
Klíčová slova keywords.txt
Kriho, J.
23. 5. 2011
Plný text práce xkriho_bc2.pdf
Kriho, J.
23. 5. 2011
Posudek oponenta kriho_bvpqbapn.pdf
Ročkai, P.
13. 6. 2011
Příloha divine.tar.gz
Kriho, J.
23. 5. 2011

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