Bakalářská práce

Simulátor pro modelovací jazyk nástroje DiVinE

Simulator for DiVinE modeling language

Martin Moráček, učo 208081
Anotace

Cílem práce je vytvoření grafického uživatelského rozhraní pro editaci a simulaci modelů systému DiVinE včetě napojení na verifikační algoritmy a simulace jimi vygenerovaných protipříkladů. Na začátku práce jsme provedli analýzu grafických rozhraní existujících nástrojů Spin a UPPAAL a navázali na ni návrhem vlastního rozhraní. Zbylá část práce popisuje vypracovanou aplikaci a její implementaci za pomocí technologie Qt.

Abstract

This work aims to create a graphical user interface for editing and simulation of models of the DiVinE system including front-end for it's verification algorithms and simulation of generated counterexamples. We have analyzed the graphical interfaces of existing verification tools Spin and UPPAAL and introduced our own design. The rest of the work describes the created application and it's implementation built upon the Qt framework.

Klíčová slova
model checking editor simulátor DiVinE DVE GUI LTL Qt
Zadání práce
Cílem projektu je vytvoření grafické aplikace (založené na technologii QT) pro editaci a simulaci modelů zapsaných v modelovacím jazyce nástroje DiVinE. Simulátor by měl spolupracovat s existujícím nástrojem DiVinE-MC, zejména by měl být schopen pro daný model nástroj spustit a poté simulovat případný protipříklad. Součástí práce bude analýza grafických simulátorů existujících verifkačních nástrojů jako jsou SPIN, UPPAAL a další.
Administrativní informace
Práce zkontrolována:
13. 1. 2010 11:29, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
934,7 KB / soubor PDF
Jazyk práce
čeština čeština
Termín obhajoby
1. 2. 2010
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK 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
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Martin Moráček FI B-IN BcIN, učo 208081 teyty/8
Moráček, M.
5. 1. 2010
Složky
Soubory
Anotace anglicky annotation_english.txt
Moráček, M.
6. 1. 2010
Anotace česky annotation.txt
Moráček, M.
6. 1. 2010
bcthesis.pdf
Moráček, M.
6. 1. 2010
bcthesis.tex
Moráček, M.
6. 1. 2010
Elektronická příloha cd-arch.zip
Moráček, M.
6. 1. 2010
Klíčová slova keywords.txt
Moráček, M.
6. 1. 2010
posudek_oponenta.pdf
Ročkai, P.
27. 1. 2010

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