Bakalářská práce

Modelování parametrizovaných systémů v jazyce DiVinE

Modelling of parametrized systems in DiVinE

Ľuboš Láska
Anotace

Cieľom práce je zhotoviť modely veťkých distribuovaných systémov, pôvodne napísaných v jazyku Promela pre verifikačný nástroj Spin, v jazyku DVE pre verifikačný nástroj DiVinE. Práca v prvej časti predstavuje jazyky Promela a DVE. V ďalšej časti poukazuje na rozdiely medzi týmito dvoma jazykmi. V poslednej časti predstavuje samotné modely a dosiahnuté výsledky.

Abstract

The aim of this bachelor thesis is to create models of large distributed systems, which were originally written in Promela language for the verification tool Spin, now in language DVE for the DiVinE verification language. In the first part languages Promela and DVE are introduced. The next part points out the differences between these two languages. The last part shows the actual models and achieved goals.

Klíčová slova
DiVinE model checking parametrizovatel’né modely Promela SPIN
Zadání práce
Cílem práce je v jazyce nástroje DiVinE namodelovat systémy, uvedené v databázi modelů pro SPIN/Promelu (http://www.albertolluch.com/promelamodels.html), které jsou parametrizovatelné. Pro každý ze systémů vytvořit sadu modelů pro různé hodnoty parametrů. Na této sadě modelů provést experimentální ověření základních vlastností (uvedených u modelů v databázi) a připravit velké modely, které není možné verifikovat s malým počtem paralelních uzlů.
Administrativní informace
Práce zkontrolována:
1. 6. 2009 13:12, prof. RNDr. Luboš Brim, CSc.
Plný text práce
204 KB / soubor PDF
Jazyk práce
slovenština slovenština
Termín obhajoby
25. 6. 2009
Práce nebyla obhájena
Student v rámci svého studia bakalářskou práci obhájil 21. 6. 2010.

Vedoucí

prof. RNDr. Luboš Brim, CSc.
abs PřF MU

Oponent

doc. RNDr. Milan Češka, Ph.D.
abs FI MU
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
Archiv závěrečné práce Ľuboš Láska FI B-AP BcAP jl3in/7
Láska, Ľ.
25. 5. 2009
Složky
Soubory
Anotace anglicky annotation_english.txt
Láska, Ľ.
25. 5. 2009
Anotace česky annotation.txt
Láska, Ľ.
25. 5. 2009
Klíčová slova keywords.txt
Láska, Ľ.
25. 5. 2009
laska_bp.pdf
Láska, Ľ.
25. 5. 2009
laska_CD.zip
Láska, Ľ.
25. 5. 2009
posudek_oponenta.pdf
Češka, M.
16. 6. 2009

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