Abstract
Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the style of LSCs and Triggered MSCs. We enrich MSCs with the possibility of using gaps (template MSC), and show their expressivity. This formalism also allows to express logical formulas. We analyze the model-checking problem, whose complexity is linear in the size of the system, and ranges from PTIME to EXPSPACE in the size of the template formula. © Springer-Verlag 2004.
Cite
CITATION STYLE
Genest, B., Minea, M., Muscholl, A., & Peled, D. (2004). Specifying and verifying partial order properties using template MSCs. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2987, 195–210. https://doi.org/10.1007/978-3-540-24727-2_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
