Archiv závěrečné práce Jindřich Babica FI N-IN IN

Mgr. Jindřich Babica

Message Sequence Chart Properties and Checking Algorithms

Message Sequence Chart Properties and Checking Algorithms

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 a s ohledem k tomuto formalismu položit základy SCStudia. Navrhli jsme datové struktury pro reprezentaci MSC, řadu nástrojů pro zpracování této struktury a zadefinovali jsme několik vlastností MSC. Spolu s těmito vlastnostmi jsme naimplementovali i kontrolní algoritmy, které ověřují nejen tyto vlastnosti, ale také i tzv. "trace race" vlastnost, která byla popsaná v samostatném článku. …víceméně

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 to study MSC and according to its notation set up basis for the SCStudio. We have designed a data structures of MSC, provided functions for their processing and defined several basic properties of MSC. We also implemented checking algorithms for these properties and trace race condition property introduced in separate paper. …víceméně

Message Sequence Chart, Basic MSC, High-level MSC, Sequence Chart Studio, SCStudio, properties of MSC, automatic check, vlastnosti MSC, automatická kontrola

Zadání: 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:

• Nastudujte ITU-T standard Z.120 popisující Message Sequence Charts (MSC); • 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. • 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. • 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. • 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 …víceméně

Jazyk práce: angličtina