Informace o projektu

Nové možnosti automatické verifikace síťových protokolů

Logo poskytovatele
Kód projektu
GP201/08/P459
Období řešení
1/2008 - 12/2010
Investor / Programový rámec / typ projektu
Grantová agentura ČR
Fakulta / Pracoviště MU
Fakulta informatiky
Klíčová slova
ověřování modelu, syntéza, formální modely

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.

Výsledky

Cílem projektu je analýza problematiky návrhu komunikačních protokolů ve variantách formalizmu Message Sequence Charts. Hlavním podcílem je výzkum v oblasti automatické kontroly takovéhoto návrhu s přihlédnutím k možnostem automatické syntézy stavových komponent takto zadaného protokolu.

Publikace

Počet publikací: 9


Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info