Diplomová práce

Coloured Nested DFS

Bc. Martin Žák
Anotace

Tato práce se zabývá implementací algoritmu CNDFS (Coloured Nested DFS) do nástroje DIVINE sloužícího k ověřování modelů. Rovněž zde shrnujeme výsledky ze srovnání algoritmu CNDFS s již implementovaným algoritmem OWCTY-MAP v prostředí sdílené paměti. Srovnání provádíme na velkém množství modelů z databáze BEEM a měříme s použitím vysokého počtu vláken. Výsledkem práce je funkční implementace algoritmu …více

Abstract

This thesis is concerned with the implementation of CNDFS (Coloured Nested DFS) algorithm into DIVINE model checking tool. Likewise, we provide comparison of the CNDFS algorithm with OWCTY-MAP algorithm, which is already implemented in the tool. The comparison takes place in shared memory environment on high number of threads. Checked models are taken from BEEM model database. The result of our work …více

Klíčová slova
Ověřování modelů Model checking Coloured Nested DFS CNDFS DIVINE LTSmin BEEM
Zadání práce
Cílem diplomové práce je implementovat paralelní algoritmus pro hledání akceptujících cyklů CNDFS (Coloured Nested DFS) v kontextu verifikačního nástroje DIVINE a porovnat výkonnost a škálovatelnost nového algoritmu s existujícími algoritmy již v nástroji DIVINE implementovanými.
Administrativní informace
Práce zkontrolována:
8. 2. 2016 15:28, RNDr. Petr Ročkai, Ph.D., učo 139761
Plný text práce
2,6 MB / soubor PDF
Jazyk práce
čeština čeština
Termín obhajoby
16. 2. 2016
Práce byla úspěšně obhájena

Vedoucí

RNDr. Petr Ročkai, Ph.D., učo 139761
KTP FI MU

Oponent

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

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná 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
 
measured measured/4
Žák, M.
11. 1. 2016
Složky
database database/4
Žák, M.
11. 1. 2016
excel excel/9
Žák, M.
11. 1. 2016
Soubory
models.tar.gz
Žák, M.
11. 1. 2016
README.txt
Žák, M.
11. 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.