Scenario Automata: theory and applications

Loïc Hélouët

loic.helouet@inria.fr

(équipe IRISA - INRIA SUMO)

(Click on the photo to start the vidéo)

Habilitation Defense - May 17th 2013

Automates d'ordres: théorie et applications

Les automates de scénarios, plus connus sous le nom de Message Sequence Charts (MSC), ont connu une énorme popularité depuis les années 1990. Ce succès est à la fois académique et industriel. Les raisons de ce succès sont multiples : le modèle est simple et s'apprend très vite. De plus il possède une puissance d'expression supérieure à celle des automates finis, et pose des problèmes difficiles. L'apparente simplicité des MSCs est en fait trompeuse, et de nombreuses questions se révèlent indécidables.
Dans cet exposé, nous reviendrons sur 10 années de recherches sur les scénarios, et tirerons quelques conclusions à partir des travaux effectués. Nous reviendrons sur les propriétés formelles des Message Sequence Charts, leur décidabilité, et les sous-classes du langage permettant la décision de certains problèmes. L'approche classique pour traiter un problème sur les MSCs est de trouver la plus grande classe possible sur laquelle ce problème est décidable.
Un autre challenge est d'augmenter la puissance d'expression des MSCs sans perdre en décidabilité. Nous proposerons plusieurs extensions des MSCs et étudierons leurs propriétés.
Nous aborderons ensuite la question d'operateurs algébriques pour les scénarios, et plus particulièrement d'opérateurs de composition. Comme tout modèle formel, les MSCs peuvent difficilement dépasser une taille critique au delà de laquelle un utilisateur ne peut plus comprendre le modèle qu'il a sous les yeux. Pour pallier à cette limite, une solution est de travailler sur de plus petits modules comportementaux, puis de les assembler pour obtenir des ensembles de comportements plus grands. Nous présenterons plusieurs mécanismes permettant de composer des MSCs, et la robustesses des sous-classes de scénarios connues à la composition.
Dans une seconde partie de cette présentation, nous étudierons des applications possibles pour les MSCs. Nous regarderons entre autres des techniques de vérification et de diagnostic, et montrerons comment ces techniques peuvent être adaptées pour la recherche de failles de sécurité dans un système distribué. Pour finir, nous tirerons quelques conclusions sur les scénarios au regard du travail de ces 10 dernières années et proposerons quelques perspectives de recherche.

Scenario automata : theory and applications

Scenario 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, it has an interesting expressive power (MSCs are for instance more expressive than finite state automata), and raises many difficult problems. Indeed, many algorithmic applications rapidly turn to be undecidable problems.
In this talk, we will sumarize a part of the work accomplished on MSCS during the last decade, and draw some conclusions from the obtained results.
We will 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. We will show several extensions to the formalism allowing dynamic creation of processes, or allowing for the design of protocols comporting sliding windows behaviors, and consider properties of these extensions.
We will then discuss some algebraic operators for scenarios, and in particular composition operators. 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 specification in a modular way, and then to assemble the modules to obtain larger sets of behaviors. We will show several mechanisms to compose MSCs, and study the robustness of MSC sub-classes with respect to composition.

In a second part of the talk, we will consider possible applications for MSCs, such as model checking problems, that can be used to discover design errors during distributed systems specification, or diagnosis. We will then show how these techniques can be adapted to find security breaches in distributed systems. Last, we will draw some conclusions on scenario models, based on the experience gained these last 10 years, and propose future research directions.

 

Les transparents (PDF)