Archiv závěrečné práce Ľuboš Korenčiak FI B-AP BcAP

Mgr. Ľuboš Korenčiak

Time Extension of Message Sequence Chart

Time Extension of Message Sequence Chart

Anotace: Message sequence charts (MSC) je grafický a textový formalizmus vhodný na na špecifikáciu distribuovanej komunikácie. Pozostáva z MSC a High-level MSC (HMSC). Formalizmus obsahuje možnosť špecifikácie času v navrhovaných systémoch. Existujú problémy nad časovými obmedzeniami v MSC, ako napríklad počítanie minimálnej siete. Prvé pokusy riešenia týchto problémov, ktoré využívajú rôzne prístupy, už boli prezentované. V tejto práci anlayzujeme rôzne prístupy k časovému rozšíreniu MSC. Ako najvhodnejší sa javí postup požívajúci labeled partially ordered sets. Je prezentované rozšírenie tohto prístupu na schpnosť formalizmu počítať minimálnu sieť. Je poskytnuté obmedzenie špecifikácie časových obmedzení na riadne obmedzena, ktoré nepovoľuje možnosť špecifikácie nejednoznačných a chybnych obmedzení. Pseudokódy algoritmov na kontrolovanie riadnych obmedzení sú poskytnuté. …víceméně

Abstract: Message sequence charts (MSC) is a graphical and textual formalism suitable for specifying distributed communication. It consists of the MSC and a High-level MSC (HMSC). The formalism incorporates the possibility of specifying time in designed systems. There arise severe problems regarding timing constraints in MSC, such as computation of minimal network. First attempts to solve the problems using various approaches have been presented. In this thesis, we analyze different approaches to time extension of MSC. As most suitable appears to be the approach using labeled partially ordered sets. An extension to this approach is provided to handle computation of minimal network in MSC formalism with coregions and constraints in HMSC. Restriction to proper constraint specification is given, which rules out ambiguous and erroneous constraint specifications. Algorithm pseudocodes for checking proper time constraints are provided. …víceméně

Message Sequence Charts, Message Sequence Graph, timing consistency, tightening, minimal network

Zadání: Formalizmus Message Sequence Chart (MSC, standard ITU-T Z.120) je navržen k popisu komunikačního chování distribuovaných entit. MSC zachycuje komunikační sekvence zasílaných zpráv. Pro přesnější (tj. realističtější) formální modelování a následné ověření korektnosti návrhu komunikačních protokolů se jako potřebné jeví rozšířit MSC o prvky časových omezení na vykonávání jednotlivých událostí. V odborné literatuře se první pokusy tohoto rozšíření již vyskytly. Úkolem studenta je:
• Nastudovat publikované přístupy k časovým rozšířením MSC. • Zhodnotit a vzájemně porovnat existující přístupy. • V případě nalezení vhodného přístupu implementovat tento do nástroje SCStudio. • V případě nenalezení vhodného přístupu navrhnout vlastní řešení k implementaci.
Při posuzování vhodnosti rozšíření je potřeba brát zřetel nejen na schopnost vyjádřit popisovaný model, ale také na možnost automaticky ověřit či vypočítat vlastnosti celkového návrhu z koeficientů jednotlivých komponent. …víceméně

Jazyk práce: angličtina