Diplomová práce

Verifikace CTL vlastností v nástroji DiVinE

CTL Model Checking in DiVinE

Bc. Šimon Vanický
Anotace

Táto práca sa zaoberá problematikou Model checkingu a paralelnými algoritmami, ktoré sa na overenie modelov používajú. Vysvetľuje dôvody, kvôli ktorým sa Model Checking používa ako formálna verifikačná metóda a základné princípy, bez ktorých sa nedá Model Checking prevádzkovať. Popisuje spôsob modelovania systémov a temporálne logiky, ktoré sa využívajú pri overovaní vlastností týchto systémov a názorne …více

Abstract

The main focus of this thesis is Model Checking and parallel algorithms that are used to formally check models of systems. It explains the reasons, why Model checking is used as a Formal Verification method and the basic principles, which are essential for running Model Checking. It describes the way of modelling systems and temporal logics that are used for verifying properties of these systems, as …více

Klíčová slova
Model Checking Formálne verifikačné metódy Kripkeho štruktúry Prechodové systémy Temporálne logiky CTL Distribuované Algoritmy Formal verification methods Kripke Structures Transition systems Temporal Logics Distributed Algorithms
Zadání práce
Cílem diplomové práce je zpracovat přehled existujích paralelních algoritmů pro automatizovanou verifikaci (model-checking) vlastností systémů v logice CTL. Vybrané algoritmy implementovat s využitím stavového generátoru nástroje DiVinE pro vícejádrové prostředí se sdílenou pamětí a provést jejich experimentální vyhodnocení a porovnání na vhodně zvolené sadě modelů. Pro porovnání zvolit odpovídající metodologii.
Administrativní informace
Práce zkontrolována:
11. 1. 2016 11:35, prof. RNDr. Luboš Brim, CSc.
Plný text práce
614,3 KB / soubor PDF
Přílohy (2)
Jazyk práce
slovenština slovenština
Termín obhajoby
16. 2. 2016
Práce nebyla obhájena
Student v rámci svého studia diplomovou práci obhájil 30. 6. 2016.

Vedoucí

prof. RNDr. Luboš Brim, CSc.
KTP FI MU

Oponent

doc. RNDr. Milan Češka, Ph.D.
abs FI MU

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
  • BRIM, Luboš; Jitka ŽIDKOVÁ a Karen YORAV. Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, roč. 7, č. 1, s. 61-73, 14 s. ISSN 1433-2779.
  • 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 Šimon Vanický FI N-IN TEI xapxq/8
Wolfová, P.
7. 12. 2015
Složky
Soubory
Anotace anglicky annotation_english.txt
Vanický, Š.
10. 1. 2016
Anotace česky annotation.txt
Vanický, Š.
10. 1. 2016
Klíčová slova keywords.txt
Vanický, Š.
10. 1. 2016
Plný text práce Diplomova_praca_Vanicky.pdf
Vanický, Š.
10. 1. 2016
Posudek oponenta posudek_oponenta_Ceska.pdf
Češka, M.
31. 1. 2016
Posudek vedoucího vanicky.pdf
Brim, L.
2. 2. 2016
Příloha CTLMC.jar
Vanický, Š.
10. 1. 2016
Příloha CTLMC.rar
Vanický, Š.
10. 1. 2016

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