Závěrečná práce: Jiří Čermák: Porovnání modelovacích schopností verifikačních nástrojů
Bakalářská práce
Porovnání modelovacích schopností verifikačních nástrojů
Comparison of verification tools capabilities
Jiří Čermák
Anotace
Cílem práce je vyzkoušet a porovnat modelovací schopnosti verifikačních nástrojů Spin, DiVinE a NuSMV na stejných typech modelů. Zejména porovnat jejich rychlost a paměťové nároky.
Abstract
The goal of this work is to try and compare the modeling capabilities of the verification tools Spin, DiVinE and NuSMV. Mainly compare their speed and memory requirements.
Zadání práce
Cilem prace je provest experimentalni porovnani vypocetni narocnosti verifikacnich nastroju SPIN, NuSMV a DiVinE. Za timto ucelem je potrebne vytvorit dostatecnou a reprezentativni sadu testovacich modelu o zhruba stejne velikosti statoveho prostoru.
Práce zkontrolována:
8. 2. 2010 08:04, prof. RNDr. Luboš Brim, CSc.
8. 2. 2010 08:04, prof. RNDr. Luboš Brim, CSc.
- Zadáno/změněno 8. 2. 2010 09:14, Helena Kryštofová
- Záznam založen 30. 11. 2009 13:31, Helena Kryštofová
- Zveřejnit od 4. 2. 2010 00:00, Helena Kryštofová
- Práce převzata 5. 2. 2010 12:06, Helena Kryštofová
Jazyk práce
čeština
Termín obhajoby
4. 2. 2010
Práce byla úspěšně obhájena
Vedoucí
prof. RNDr. Luboš Brim, CSc.
abs PřF MU
abs PřF MU
Studijní program
Informatika
Obor
Práce na příbuzné téma
Seznam prací, které mají shodná klíčová slova.
-
Porovnání nástrojů pro paralelní LTL model checking
Mgr. Marek Tomáštík, učo 374575 -
Simulátor pro modelovací jazyk nástroje DiVinE
Bc. Martin Moráček, učo 208081 -
Predicate Abstraction of DiVinE Models
Mgr. Jiří Novosad, učo 99288 -
Graficke rozhraní pro komunikaci s nástrojem DiVinE
RNDr. Vojtěch Forejt, Ph.D., LL.B. (Hons) -
API pro monitorování chování programů v kontextu nástroje DIVINE
Mgr. Tadeáš Kučera, učo 423907 -
Post-mortem analýza stavového prostoru
Mgr. Jan Kriho -
Untimed LTL Model Checking of Timed Automata
Mgr. Jan Havlíček -
Verifikační manažer pro explicitní ověřování modelu
Mgr. Václav Rosecký
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Jiří Čermák FI B-IN BcIN bd6oj/10
Čermák, J.
4. 1. 2010
Složky
Soubory
-
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.