Disertační práce

Automating Software Development with Explicit Model Checking

Mgr. Petr Bauch
Anotace

Tato práce je postavená na předpokladu, že funkční požadavky je možné vyjádřit temporální logikou a obsahem této práce jsou nové způsoby verifikace jak požadavků samotných tak jejích splnění běhěm celého vývojového procesu. Cílem práce je automatizace některých verifikačních procesů, které se v současné době používají během vývoje programů. Hlavním prostředkem pro dosažení tohoto cíle je technika ověřování …více

Abstract

This thesis builds on the fact that functional requirements can be expressed in temporal logic and we propose new means of verifying the requirements themselves and the compliance to those requirements throughout the development process. The goal is the automation of some of the verification processes currently employed in software development. The tool is the automata-based, explicit-state model checking …více

Klíčová slova
sanity checking model checking satisfiability modulo theories
Administrativní informace
Práce zkontrolována:
16. 11. 2015 07:48, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
1,1 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
18. 2. 2016
Práce byla úspěšně obhájena

Vedoucí

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

Oponenti

doc. RNDr. Jan Kofroň, Ph.D.
MFF UK v Praze
Assoc. Prof. Keijo Heljanko
School of Science, Aalto University, Finland
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika (čtyřleté)
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.