2008Langages de Scénarios: Utiliser des Ordres Partiels pour Modéliser, Vérifier et Superviser des Systèmes Parallèles et Répartis.
Ph.D. Thesis, University of Rennes 1.
Abstract. Our work is dedicated to the modeling and the analysis of concurrent and distributed systems. More precisely, we seek to model, verify and supervise systems composed by autonomous entities which interact locally through shared memory and globally through asynchronous message passing. In this context, we argue that, instead of modeling each entity independently and then analyzing what happens when all of them interact, it is better to have a complete theory to globally describe a concurrent system, in which verification and supervision analysis are decidable. This theory is based on partially ordered multisets (ie. “pomsets”) which is a “true-concurrency” model. To this end, we defined the causal hmsc model, based on pomsets and which extends the standardized hmsc formalism with constructs from Mazurkiewicz trace theory. We first show that a syntactic restriction of causal hmsc is equivalent to bounded mixed automata, a formalism which extends Zielonka asynchronous automata and communicating finite state machines. We also show that classical model-checking techniques can be extended to pomsetsbased formalisms without losing efficacy. This is an important result, as pomsets-based formalisms, such as causal hmsc, are more concise than sequential system formalisms. Finally, we propose efficient methods to analyse large recorded files from distributed executions and we propose supervision techniques such as diagnosis and event correlation, using pomsets-based models of distributed and concurrent systems.