Bakalářská práce

Porovnání nástrojů pro paralelní LTL model checking

Comparison of parallel LTL model checkers

Marek Tomáštík, učo 374575
Anotace

V práci je představeno výkonové porovnání vybraných nástrojů pro model checking, které se soustředí na explicitní model checking, ověřování vlastností specifikovaných v LTL, a především na paralelní a distribuovanou verifikaci (testovány jsou nástroje DiVinE, LTSmin, PReach a Spin). Je připravena sada instancí pro testování, ve které jsou pro všechny modely zahrnuty verze v každém z hlavních modelovacích …více

Abstract

This work presents a performance comparison of model checking tools that focus on explicit model checking, verification of LTL properties, and mainly on parallel and distributed verification (the tested tools are DiVinE, LTSmin, PReach, and Spin). A set of test instances is prepared, where every model is given in each of the main modelling languages used by the tested tools, with the aim of the different …více

Klíčová slova
model checking LTL comparison benchmark DiVinE Spin LTSmin PReach
Zadání práce
Cílem práce je porovnat současné nástroje pro paralelní model checking LTL vlastností. Konkrétně se jedná o nástroje DiVinE, SPIN, PREACH, LTSmin, SPINS a případně další. Pro porovnání je potřebné navrhnout vhodnou metodiku a vytvořit vhodnou sadu testů, které by byly dostatečně velké a nebylo je možné verifikovat s malým počtem paralelních uzlů/vláken.
Administrativní informace
Práce zkontrolována:
21. 5. 2013 08:12, prof. RNDr. Luboš Brim, CSc.
Plný text práce
1,4 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
17. 6. 2013
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
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

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