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

Untimed LTL Model Checking of Timed Automata

Bc. Jan Havlíček
Anotace

Tato práce popisuje novou možnost verifikovat časové automaty, která byla implementována do paralelního model checkeru DiVinE. Ta umožňuje, aby DiVinE verifikoval LTL vlastnosti modelů časově kritických systémů vytvořených v UPPAALu. Součástí práce je také přehled abstrakcí a redukčních technik, které jsou požívány při zpracování časových automatů a jejich rozšíření, a diskuze nad jejich použitelnosti …více

Abstract

This thesis presents a new option to verify timed automata that has been implemented into the parallel model checker DiVinE. This allows DiVinE to verify LTL properties on models of real-time systems designed by UPPAAL. We overview abstractions and reduction techniques commonly used in verification of timed automata and their extensions and discuss their usability for LTL model checking. We also perform …více

Klíčová slova
Timed Automata Model Checking Verification Parallel DiVinE UPPAAL LTL
Zadání práce
The aim of this Master's thesis is to extend model checker DiVinE with the ability of parallel and distributed LTL model checking of timed automata. In particular, the thesis will define various zone-based abstractions that are used to enable efficient model checking procedure for timed automata and will investigate how the abstractions can be combined with automata-based approach to LTL model checking. The implementation within DiVinE should be evaluated on selected examples of real-time systems as distributed with the UPPAAL verification tool.
Administrativní informace
Práce zkontrolována:
23. 5. 2013 14:35, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
582,3 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
26. 6. 2013
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

prof. RNDr. Ivana Černá, CSc., učo 1419
KTP FI MU

Literatura

  • BAIER, Christel a Joost-Pieter KATOEN. Principles of model checking. Cambridge, Mass.: MIT Press, 2008, xvii, 975. ISBN 9780262026499.
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 Havlíček FI N-IN PDS mohwa/6
Kryštofová, H.
14. 3. 2013
Složky
Soubory
Anotace anglicky annotation_english.txt
Havlíček, J.
15. 5. 2013
Anotace česky annotation.txt
Havlíček, J.
15. 5. 2013
Klíčová slova keywords.txt
Havlíček, J.
15. 5. 2013
Plný text práce thesis.pdf
Havlíček, J.
15. 5. 2013
Posudek DP DP_Havlicek
Dvořáčková, H.
1. 7. 2013
Posudek oponenta posHavlicek.pdf
Černá, I.
10. 6. 2013

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