Diplomová práce

LTL atraktory

LTL attractors

Bc. Peter Bezděk
Anotace

Táto diplomová práca sa zaoberá rozšírením overovania modelov konečne stavových systémov pre formule lineárnej temporálnej logiky (LTL) o verifikáciu platnosti formule LTL pre viaceré stavy systému. V práci zadefinujeme pojem LTL atraktoru, ktorý bude reprezentovať takú množinu stavov systému, ktorej prvky splňujú danú formulu LTL. V rámci práce navrhneme a implementujeme sekvenčný a paralelný algoritmus …více

Abstract

This master thesis aims to extend model checking of finite state systems for linear temporal logic (LTL) with the verification of LTL formulas for set of states of system. We define the LTL attractor as a set of states which satisfy the given LTL formula. To find LTL attractor we design and implement the sequential and parallel algorithm. The implementation is experimentally evaluated for several models …více

Klíčová slova
lineárna temporálna logika LTL overovanie modelov model checking automatická verifikácia protipríklad vysvetlenie chyby LTL atraktor atraktor atrakčná množina Nested DFS silne súvislé komponenty OBF
Zadání práce
Cílem diplomové práce je formálně zadefinovat pojem atraktoru pro formule lineární temporální logiky (LTL) a popsat jeho roli v kontextu verifikace systémů metodou ověřování modelu (model checking). Zejména bude v práci diskutována souvislost LTL atraktorů s problematikou nalezení a interpretace vícero protipříkladů LTL formule. Součástí práce bude nalezení a klasifikace algoritmů pro výpočet LTL atraktorů a jejich experimentální vyhodnocení.
Administrativní informace
Práce zkontrolována:
1. 6. 2009 10:48, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
663,9 KB / soubor PDF
Jazyk práce
slovenština slovenština
Termín obhajoby
29. 6. 2009
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
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 Peter Bezděk FI N-IN IN qjn7v/7
Bezděk, P.
24. 5. 2009
Složky
Prílohy práce (program, modely, ...) appendix/4
Bezděk, P.
24. 5. 2009
Soubory
Anotace anglicky annotation_english.txt
Bezděk, P.
24. 5. 2009
Anotace česky annotation.txt
Bezděk, P.
24. 5. 2009
Klíčová slova keywords.txt
Bezděk, P.
24. 5. 2009
Posudek oponenta posudek_oponenta.pdf
Černá, I.
9. 6. 2009
Text práce master_thesis.pdf
Bezděk, P.
24. 5. 2009

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