Project information
New possibilities in automatic verification of network protocols
- Project Identification
- GP201/08/P459
- Project Period
- 1/2008 - 12/2010
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Postdoctoral projects
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- model checking, synthesize, verification, formal models
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 MSC such that it can express important design features and, at the same time, it preserves decidability of significant verification questions.
Results
Publications
Total number of publications: 9
2012
-
Almost linear Büchi automata
Mathematical Structures in Computer Science, year: 2012, volume: 22, edition: 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, year: 2011
2010
-
Almost Linear Büchi Automata
Year: 2010, type: Appeared in Conference without Proceedings
-
Decidable Race Condition and Open Coregions in HMSC
Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010), year: 2010
-
Stochastic Real-Time Games with Qualitative Timed Automata Objectives
CONCUR 2010 - Concurrency Theory, year: 2010
2009
-
Almost Linear Büchi Automata
Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09), year: 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), year: 2009
-
Reachability is decidable for weakly extended process rewrite systems
Information and Computation, year: 2009, volume: 207, edition: 6
2008
-
Petri Nets Are Less Expressive Than State-Extended PA
Theoretical Computer Science, year: 2008, volume: 394, edition: 1-2