Archiv závěrečné práce Martin Chmelík FI B-IN BcIN

Mgr. Martin Chmelík

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

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

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 obecně, ale je možné algoritmicky rozhodnout, zda je možné jej použít. V negativním případě algoritmus označí příčiny. …víceméně

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 approach cannot be applied in general, but we can algorithmically decide, whether our approach is appliable. Moreover, when we cannot apply our approach, we may advise the designer, what is causing the inapplicableness. …víceméně

MSC, message sequence chart, MSG, message sequence graph, HMSC, high-level message sequence chart, hierarchical message sequence chart, NLC, non-local choice

Zadání: 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. …víceméně

Jazyk práce: angličtina