Bakalářská práce

Deciding Non-local Choice in High-level Message Sequence Charts

Martin Chmelík
Anotace

Nelokální volba ve formalizmu Message Sequence Chart způsobuje nežádoucí a nespecifikovaná chování v implementovaném systému. Tato práce se zaměřuje na problematiku nelokální volby v High-level Message Sequence Chart specifikacích. Navrhujeme algoritmus na detekci míst s nelokální volbou. Přinášíme nový přístup v řešení nelokálních voleb pomocí dodatečných požadavků na systém. Přístup nelze uplatnit …více

Abstract

Non-local choice property in Message Sequence Chart formalism is causing unwanted and unspecified behavior in the implemented system. This work focuses on detecting non--local choice in High--level Message Sequence Chart specifications. We propose an algorithm that detects non--local choice. We introduce a new approach to deal with non--local choice, by having further assumptions on the system. The …více

Klíčová slova
MSC message sequence chart MSG message sequence graph HMSC high-level message sequence chart hierarchical message sequence chart NLC non-local choice
Zadání práce
Při návrhu nových aplikací pro komunikující distribuované systémy 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 (např. problém race condition a non-local choice).

Spolu s průmyslovými partnery jsme jako vhodný formalismus vybrali Message Sequence Charts (MSC) a zvláště pak rozšířenou variantou High-level Message Sequence Charts (HMSC). Oba tyto formalizmy byly zavedeny v ITU specifikaci Z.120.

Úkolem studenta je zaměřit se na problém detekce nelokální volby (non-local choice), řádně nastudovat, jaké problémy tato vlastnost v návrhu způsobuje a pokusit se vyvinout algoritmus pro detekci míst v návrhu, které mohou nelokální volbu rozhodnout, tj. hlavně distribuovat své rozhodnutí aktérům volby (následníkům v navržené komunikační sekvenci).

V případě úspěchu může být tento algoritmus implementována a dodán do nástroje Sequence Chart Studio (SCStudio), který je pod licencí LGPL vyvíjen studenty FI.

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

  • Nastudujte ITU-T standard Z.120 popisující Message Sequence Charts (MSC).
  • Prozkoumejte publikované možnosti automatického ověřování non-local choice.
  • Zamyslete se nad detekcí míst v návrhu, které mohou rozhodovat nelokální volby.
  • Navrhněte algoritmus na detekci míst v návrhu, které mohou rozhodovat nelokální volby.
Administrativní informace
Práce zkontrolována:
27. 5. 2009 09:39, doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
Plný text práce
315,5 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
25. 6. 2009
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

RNDr. Vojtěch Forejt, Ph.D., LL.B. (Hons)
abs 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 Chmelík FI B-IN BcIN jtl53/6
Chmelík, M.
24. 5. 2009
Složky
Soubory
Anotace anglicky annotation_english.txt
Chmelík, M.
24. 5. 2009
Anotace česky annotation.txt
Chmelík, M.
24. 5. 2009
Klíčová slova keywords.txt
Chmelík, M.
24. 5. 2009
posudek_oponent posudek_oponent.odt
Forejt, V.
17. 6. 2009
thesis.pdf
Chmelík, M.
24. 5. 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.