Diplomová práce

API pro monitorování chování programů v kontextu nástroje DIVINE

API for Monitoring of Program Behaviour in DIVINE Model Checker

Bc. Tadeáš Kučera, učo 423907
Anotace

V této práci se zabýváme návrhem a implementací API pro monitorování programů verifikačním nástrojem DIVINE. Implementovaný monitor podporuje monitorování omega-regulárních vlastností programu pomocí zobecněných Buchiho automatů s akceptační podmínkou na hranách (TGBA). Naše rozhraní nabízí specifikaci přímo ve formě TGBA nebo ve formě formulí lineární temporální logiky (LTL), a to prostřednicvím vlastního …více

Abstract

In this work, we design and implement the API for program monitoring by the model checker DIVINE. The implemented monitor supports the monitoring of omega-regular properties using generalized transition based Buchi automata. Our implementation enables the specification of required properties in the form of TGBA or via a formula in linear temporal logic (LTL). We implement a custom translation engine …více

Klíčová slova
formal verification model checking DIVINE LTL Buchi Automata implementation C++ formální verifikace ověřování modelu Buchiho automaty implementace
Zadání práce
Cílem diplomové práce je nejprve návrh C/C++ API pro monitorování chování programů v kontextu formálního verifikačního nástroje DIVINE, a následně prototypová implementace monitoru a jeho integrace do nástroje DIVINE. Implementovaný monitor musí podporovat monitorování omega regulárních vlastností programů, které jsou typicky zadané pomocí konečných automatů s Buchi akceptační podmínkou na stavech, nebo na hranách. Prototypová implementace musí také ve výsledku umožnit nástroji DIVINE verifikaci programů vůči specifikaci programových vlastností zadaných formulemi lineární temporální logiky (LTL), což potažmo může vyžadovat realizaci vlastního překladu formulí LTL na Buchi automaty, nebo zapojení existujících překladačů do prototypové implementace. Součástí diplomové práce bude alespoň jedna případová studie, která demonstruje funkcionalitu implementovaného prototypu.
Administrativní informace
Práce zkontrolována:
11. 1. 2019 15:41, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
4,9 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
6. 2. 2019
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

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

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.
  • VARDI, M. Automata-Theoretic Model Checking Revisited. Proc. of Verification, Model Checking and Abstract Interpretation (VMCAI'07). Vol. 4349 of LNCS. Springer, 2007.
Citovat tuto práci
Masarykova univerzita Přírodovědecká fakulta
Studijní program
Matematika
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.