Bachelor's thesis

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

Martin Chmelík
Abstract

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 …more

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 …more

Keywords
MSC message sequence chart MSG message sequence graph HMSC high-level message sequence chart hierarchical message sequence chart NLC non-local choice
Thesis description
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.
Administrative information
The thesis has been checked:
27/5/2009 09:39, doc. RNDr. Vojtěch Řehák, Ph.D., UČO 3721
Full text of thesis
315,5 KB / file PDF
Language used
English English
Defence date
25/6/2009
The thesis was defended successfully

Supervisor

doc. RNDr. Vojtěch Řehák, Ph.D., UČO 3721
KTP FI MU

Reader

RNDr. Vojtěch Forejt, Ph.D., LL.B. (Hons)
abs FI MU
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

Similar documents
 
Name
Posted by
Uploaded/Created
Rights
Archive of Thesis/Dissertation Martin Chmelík FI B-IN BcIN jtl53/6
Chmelík, M.
24/5/2009
Folders
Files
Abstract (in English) annotation_english.txt
Chmelík, M.
24/5/2009
Abstract (in Czech) annotation.txt
Chmelík, M.
24/5/2009
Keywords 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.