Diplomová práce

Message Sequence Chart Properties and Checking Algorithms

Bc. Jindřich Babica
Anotace

Message Sequence Chart (MSC) je hojně používaný formalismus pro popis telekomunikačních systémů. Nedostatek kvalitních nástrojů pro zpracování tohoto formalismu nás vedlo k vytvoření nového nástroje -- Sequence Chart Studio (SCStudio). Tento nástroj by neměl sloužit jen k návrhu systému pomocí MSC, ale zároveň také k ověření některých vlastností tohoto návrhu. Cílem této práce bylo nastudovat MSC …více

Abstract

Message Sequence Chart (MSC) is a widely used formalism for description of telecommunication systems. A lack of tools to support MSC led us to start development of a new tool -- Sequence Chart Studio (SCStudio). Using this tool one should be capable to design a system in the MSC notation, moreover, the tool will provide automatic checks of several properties of the system. The aim of this thesis was …více

Klíčová slova
Message Sequence Chart Basic MSC High-level MSC Sequence Chart Studio SCStudio properties of MSC automatic check vlastnosti MSC automatická kontrola
Zadání práce
Při návrhu nových aplikací se používají různé modelovací jazyky, které slouží jednak k přehlednému a systematickému zápisu, ale hlavně umožňují do vývojového cyklu aplikací zapojit automatizované metody hledání chyb a ověřování korektnosti. Jako vhodný modelovací jazyk pro návrhy síťových protokolů jsme spolu s průmyslovými partnery vybrali Message Sequence Charts (MSC).

Cílem našeho projektu SCStudio je definovat vhodné modifikace MSC tak, aby se zvýšila použitelnost při modelování, ale zároveň byla zachována možnost ověření korektnosti návrhu. Dále je naším cílem nalézt a implementovat účinné a použitelné algoritmy ověřování. Vše bude zakomponováno do nově vznikajícího otevřeného nástroje, který umožní jak přehledné a pohodlné vytváření návrhů protokolů v MSC, tak automatickou kontrolu správnosti a automatickou detekci případných chyb v návrhu. Projekt je realizován v přímé spolupráci se společností ANF DATA (Siemens AG Österreich), která se vývojem aplikací pro mobilní sítě dlouhodobě zabývá.

Cílem této práce je seznámit se se standardem ITU Z.120, který definuje podobu MSC. Dále student vyhledá ve sbornících vědeckých konferencí publikované možnosti automatického ověřování správnosti a hledání chyb v MSC návrzích. Je potřeba dávat zvláště pozor na to, že MSC užívané v oblasti teoretické informatiky se může výrazně lišit od definice ITU Z.120. Vhodné algoritmy pak student implementuje.

Dílčí úkoly a požadavky:

  1. Nastudujte ITU-T standard Z.120 popisující Message Sequence Charts (MSC);
  2. Prozkoumejte publikované možnosti automatického ověřování korektnosti a hledání chyb, zaměřte se při tom na takové, které splňují popis podle ITU Z.120. V případě nesouladu s ITU Z.120 se pokuste algoritmy upravit tak, aby fungovaly i pro tuto mezinárodně uznanou specifikaci.
  3. Dobře rozmyslete a položte základy SCStudia tak, aby byly možné pohodlně implementovat verifikační algoritmy nad MSC. Navrhněte datové struktury vhodné pro práci s MSC. Implementujte (traverse) algoritmy pro účely procházení datových struktur společně s příslušnými posluchači (listeners) událostí, které nastávají při procházení datových struktur.
  4. Vybrané algoritmy implementujte v programovacím jazyku C++ tak, aby pracovali s MSC podle specifikace ITU Z.120 a byly použitelné v rámci vznikajícím projektu SCStudio.
  5. Kód musí být licencován GNU Lesser General Public License (LGPL) verze 2.1.
Literatura a odkazy:

[1] Message Sequence Charts (MSC), ITU-T recommendation Z.120 (04/2004)

[2] SCStudio, http://sourceforge.net/projects/scstudio

Administrativní informace
Práce zkontrolována:
6. 1. 2009 07:04, (IS automaticky)
Plný text práce
643,2 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
9. 2. 2009
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
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 Jindřich Babica FI N-IN IN pon4r/8
Babica, J.
4. 1. 2009
Složky
Soubory
Anotace anglicky annotation_english.txt
Babica, J.
4. 1. 2009
Anotace česky annotation.txt
Babica, J.
4. 1. 2009
CD cd.zip
Babica, J.
5. 1. 2009
Klíčová slova keywords.txt
Babica, J.
4. 1. 2009
Master thesis source thesis.tex
Babica, J.
4. 1. 2009
Master thesis thesis.pdf
Babica, J.
4. 1. 2009
posudek_oponent posudek_oponenta.pdf
Gotthard, P.
22. 1. 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.