Diplomová práce

New checkers for Sequence Chart Studio

Bc. Václav Vacek, učo 172426
Anotace

Pro specifikace komunikace se často užívá formalismus zvaný Message Sequence Chart. Ačkoliv vznikl pro oblast telekomunikací, jeho použití je všestranné. Tým studentů Fakulty informatiky vyvíjí aplikaci pro kreslení a verifikaci MSC - Sequence Chart Studio (SCStudio). Tato práce popisuje částo tohoto vývoje: Existující verifikační algoritmy byly revidovány a opraveny a bylo implementováno pět algoritmů …více

Abstract

For the specification of communication between entities, the formalism called Message Sequence Chart is often used. Even though it originates from the telecommunication area, its usage is not limited to it. A team of students at the Faculty of Informatics has been developing an application for drawing and verifying Message Sequence Charts called Sequence Chart Studio (SCStudio). This thesis describes …více

Klíčová slova
Message Sequence Chart MSC Sequence Chart Studio SCStudio verification model of communication model checking LTL race condition local choice boundedness
Zadání práce
Tým studentů FI MUNI vyvíjí aplikaci Sequence Chart Studio, která umožní kreslit a verifikovat MSC (standard ITU-T Z.120) a UML sekvenční diagramy.

Cílem této práce je:

  • detailně revidovat stávající kontrolní algoritmy (acyclic, deadlock, livelock, FIFO, race),
  • odstranit zjištěné nedostatky (reimplementace, doplnění testovacích příkladů, vylepšení dokumentace),
  • navrhnout a implementovat nové verifikační algoritmy (boundedness, local choice, recursivity, name checker, strong realizability) a exportní filtr do formátu DiVinE (realizace MSC návrhu).

Aplikace musí být implementována v C/C++ a licencována GNU Lesser General Public License (LGPL). Textová část práce by měla být psána anglicky (není podmínkou).

Literatura:

  • Jindřich Babica, Message Sequence Charts; Properties And Checking Algorithms, Master Thesis, Masaryk University, Brno, January 2009.
  • Vojtěch Řehák, Petr Slovák, Jan Strejček, and Loïc Hélouët. Decidable Race Condition for HMSC. Technical Report FIMU-RS-2009-10, 30pp, Faculty of Informatics, Masaryk University, 2009.
Administrativní informace
Práce zkontrolována:
11. 1. 2011 08:53, doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
Plný text práce
536 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
9. 2. 2011
Práce byla úspěšně obhájena

Vedoucí

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
KTP FI MU

Oponent

Ing. Petr Gotthard

Konzultant

Ing. Petr Gotthard

Literatura

  • GENEST, B.; A. MUSCHOLL; H. SEIDL a M. ZEITOUN. Infinite-State High-Level MSCs: Model-Checking and Realizability. Journal of Computer and System Sciences. Elsevier, 2006, roč. 72, č. 4, s. 617-647.
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 Václav Vacek FI N-IN TEI, učo 172426 asieu/9
Vacek, V.
10. 1. 2011
Složky
Soubory
Anotace anglicky annotation_english.txt
Vacek, V.
10. 1. 2011
Anotace česky annotation.txt
Vacek, V.
10. 1. 2011
Klíčová slova keywords.txt
Vacek, V.
10. 1. 2011
Posudek oponent posudek_vacekDP.pdf
Gotthard, P.
4. 2. 2011
SCStudio installer scstudio.exe
Vacek, V.
10. 1. 2011
SCStudio source scstudio.zip
Vacek, V.
10. 1. 2011
The thesis proper thesis.pdf
Vacek, V.
10. 1. 2011
Thesis source thesis.zip
Vacek, V.
10. 1. 2011

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