The aim of the project is to study formalisms for network comunication system specification at a very early stage of design. Variety of studies has been done on Message Sequence Charts (MSC) formalism in this research area. Eventhough MSC is formaly specified in ITU Recomendation Z.120, most of the theoretical results deals with some subsets of this formalism only. On the other hand, there are many undecidability results related to the MSC in its full expressivity. Our aim is to find a subset of MSCsuch that it can express important design features and, at the same time, it preserves decidability of significant verification questions. (en)
Cílem projektu je studium formalizmů pro popis specifikace síťových komunikačních systémů relevantních pro počáteční fáze návrhu projektu. Jako poměrně vhodným formalizmem se v posledních letech výzkumu jeví Message Sequence Charts (MSC). Přestože je tento formalizmus přesně specifikován podle ITU Recomendation Z.120, ve většině teoretických článků je uvažována pouze jistá podmnožina této specifikace. Naopak pro plnou specifikační sílu MSC byly většinou publikovány výsledky týkající se nerozhodnutelnosti. Cílem projektu bude nalezení vhodné varianty či modifikace MSC, která si zachová rozumné vyjadřovací schopnosti a zároveň však bude možné systémy takto specifikované automaticky verifikovat. (cs)