Scenario automata : theory and applications

Partial order automata are more known under their standardized name "'Message Sequence Charts (MSCs). They have met a considerable interest during the last 15 years. This success is both industrial and academic, and has several reasons. First, the model is rather simple and can be learned very easily by engineers. Second, despite its apparent simplicity (MSCs are for instance more expressive than finite state automata), it has an interesting expressive power, and raises many difficult problems. Indeed, many algorithmic applications rapidly turn to be undecidable problems. In this document, we collect and sumarize a part of the work accomplished on MSCS during the last decade, and draw some conclusions from the obtained results. We first focus on formal properties of MSCs, the decidability of several standard problems, and the definition of subclasses of the language allowing for the decision of some problems when the general case is undecidable. The standard approach to work with MSCs is to find the larger subclass of the language allowing for the decision of a given problem. Another challenge is to increase the expressive power of MSCs without loosing decidability of too many problems. We propose several extensions to the formalism allowing dynamic creation of processes, or allowing for the design of protocols comporting sliding windows behaviors. As many formal models, MSCs can not exceed a limit size after which a diagram is not understandable for a human designer. A solution is then to build a specifcation in a modular way, and then to assemble the modules to obtain larger sets of behaviors. We propose several mechanisms to compose MSCs, and study the robustness of MSC sub-classes to composition. We then draw some conclusions from the properties of composition mechanisms described in this part of the document. Overall, composition is seldomly effective, and does not preserve formal properties of partial order automata. In a second part of this document, we study possible applications for MSCs. We consider model checking problems, that can be used to discover design errors during distributed systems specification. The second application considered is diagnosis, which allows to retreive out of a model the explanations of some partial observation of an instrumented system. Last, we consider the applicability of MSCs to the search for security breaches in distributed systems. To complete the work, we provide some conclusions on scenario models, based on the content of this document and on the experience gained these last 10 years. We then propose future research directions.

Data and Resources

Additional Info

Field Value
Source https://theses.hal.science/tel-00926742
Author Hélouët, Loïc
Maintainer CCSD
Last Updated May 7, 2026, 13:35 (UTC)
Created May 7, 2026, 13:35 (UTC)
Identifier tel-00926742
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor SUpervision of large MOdular and distributed systems (SUMO) ; Centre Inria de l'Université de Rennes ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) ; Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
creator Hélouët, Loïc
date 2013-05-17T00:00:00
harvest_object_id 055dc802-164f-400e-9527-a93046adaa12
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-02-07T00:00:00
set_spec type:HDR