Informace o projektu
Nové možnosti automatické verifikace síťových protokolů
- Kód projektu
- GP201/08/P459
- Období řešení
- 1/2008 - 12/2010
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Postdoktorské projekty
- 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
2012
-
Almost linear Büchi automata
Mathematical Structures in Computer Science, rok: 2012, ročník: 22, vydání: 2, DOI
2011
-
Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, rok: 2011
2010
-
Almost Linear Büchi Automata
Rok: 2010, druh: Další prezentace na konferencích
-
Decidable Race Condition and Open Coregions in HMSC
Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010), rok: 2010
-
Stochastic Real-Time Games with Qualitative Timed Automata Objectives
CONCUR 2010 - Concurrency Theory, rok: 2010
2009
-
Almost Linear Büchi Automata
Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09), rok: 2009
-
On Decidability of LTL+Past Model Checking for Process Rewrite Systems
Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008), rok: 2009
-
Reachability is decidable for weakly extended process rewrite systems
Information and Computation, rok: 2009, ročník: 207, vydání: 6
2008
-
Petri Nets Are Less Expressive Than State-Extended PA
Theoretical Computer Science, rok: 2008, ročník: 394, vydání: 1-2