Message Sequence Charts (MSC) je standardizovaný formalismus pro popis chování (tele)komunikačních systémů. Standard Z.120 definuje jeho grafickou a textovou podobu. Při návrhu specifikace systému je výhodnější používat grafickou podobu, protože je názornější a pro člověka čitelnější. Tým studentů ve spolupráci se společností ANF DATA (Siemens AG Österreich) si dal za cíl vyvinout nástroj, který by již v době vzniku specifikace komunikačního systému dokázal pomocí vhodných algoritmů odhalit chyby ve vznikajícím návrhu MSC.

Úkolem studenta je zjistit dostupnost existujících nástrojů pro práci s Message Sequence Charts (MSC). Při výběru nástojů je potřeba se zaměřit zvláště na dostupnost, komfort modelování a podporované vyjadřovací možnosti implementované varianty MSC. Dalším nezanedbatelným měřítkem jsou možnosti automatického ověření specifických vlastností navržených MSC (fifo, local choice, race condition, ...) spolu s přehledností výstupů z těchto ověření včetně případných chybových hlášení. Ze zkoumaných nástrojů pak student vybere několik s vhodnými vlastnostmi a přehledně popíše jejich výhody i nedostatky.

Na základě získaných zkušeností pak student navrhne nový nástroj, ve kterém vhodně zkombinuje nejlepší vlastnosti zkoumaných nástrojů. Tento detailní návrh bude podkladem pro programátory, kteří jej implementují.

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

1. Nastudujte ITU-T standard Z.120 popisující MSC;
2. Prozkoumejte a přehledně porovnejte možnosti existujících nástrojů pro modelování a ověřování návrhů v modelovacím jazyce MSC;
3. Navrhněte vlastní nástroj, který umožní vytvářet MSC a ověřovat zajímavé vlastnosti;

Literatura:

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