Modelling and analysing open reconfigurable systems

• Main Author: Pham, Viet Van
• Other Authors: Evry-Val d'Essonne
• Language: en
• Published: 2014
• Subjects: Pi-graphes
• Online Access: http://www.theses.fr/2014EVRY0059/document

Les systèmes ouverts reconfigurables sont aujourd'hui omniprésents dans le paysage informatique : réseaux mobiles, calculs et données dans “le nuage”, etc. Une particularité de ces systèmes est que leur topologie de communication évolue dynamiquement - nous parlerons de reconfiguration - en conséquence d'activités concurrentes internes ou externes. Les systèmes de transitions étiquetées pour les systèmes ouverts permettent de prendre en considération l'environnement extérieur de façon implicite.Les systèmes ouverts reconfigurables sont souvent modélisés par des formalismes inspirés ou dérivés du π-calcul. Le passage de nom permet de modéliser la dynamique des topologies de communication. Dans cette thèse, nous introduisons les π-graphs, une variante du π-calcul qui possède, entre autre, une interprétation graphique naturelle. De plus, le formalisme a été conçu pour servir de langage intermédiaire entre le π-calcul abstrait et des formalismes plus concrets, en particulier dans la famille des réseaux de Petri de haut-niveau.Nous proposons tout d'abord une traduction formelle et prouvée des π-graphes vers des réseaux de Petri de haut niveau supportés par des outils de modélisation et de vérification courants. Nous montrons que cette traduction peut-être élevée au rang d'isomorphisme entre les deux formalismes. Ainsi, les outils prototypes que nous avons développés dans le cadre des π-graphes peuvent travailler de concert avec des outils plus stables et plus généraux basés sur les réseaux de Petri.En se basant sur cette traduction bi-directionnelle, nous développons une extension de la logique temporelle linéaire (LTL) - la logique des systèmes ouverts reconfigurables - permettant de spécifier des propriétés portant sur la dynamique d'évolution de la topologie de communication dans le cadre d'environnements ouverts. Les propositions atomiques de cette logique caractérisent précisément les propriétés d'état des π-graphs.Un prototype d'outil a été développé dans le cadre de cette thèse pour valider expérimentalement l'approche proposée. Cet outil fournit un simulateur pour les modèles exprimés dans le formalisme des π-graphes. Ces modèles peuvent être compilés en réseaux de Petri de haut niveau et manipulés dans le cadre de l'outil SNAKES. Enfin, nous proposons une traduction de la logique des systèmes ouverts reconfigurables vers la logique de plus bas niveau supportée par le vérificateur de modèle NECO. Grâce à notre prévue constructive d'isomorphisme entre les π-graphes et leur traduction en réseaux de Petri, les contre-exemples générés pour les réseaux de Petri en cas d'invalidation de proposition par NECO peuvent être réinterprétées et expliquées dans les termes des π-graphes. === Today we witness the rapid spread of highly dynamic reconfigurable and distributed infrastructures that we group under the common name of open reconfigurable systems. The communication topology of those systems can dynamically change - or reconfigure - as a consequence of an internal or external concurrent activity. Labelled transition semantics for open systems allow to take into account the external activities in an implicit way.Open reconfigurable systems are commonly modeled using formalisms inspired by the π-calculus. Name passing makes it possible to model dynamic communication topologies. In this thesis, we introduce the π-graphs, a variant of the π-calculus that among other things enjoys a natural graphical interpretation. Moreover, the formalism has been designed to serve as an intermediate language between the abstract π-calculus and more concrete realizations, especially in the realm of high-level Petri nets.We first propose a faithful encoding of π-graphs into high-level Petri nets that are supported by common modelling and verification tools. We show that the translation can be lifted to an isomorphism between the two formalisms. Hence, the prototype tools that are developed specifically for π-graphs can be used in conjunction with more mature and general tools for Petri nets.Based on this bidirectional encoding, we develop a high-level variant of the linear temporal logic - namely the open system logic - to specify properties about the dynamic evolution of systems taking into account interactions within open environments. The atomic propositions of the logic precisely capture the state properties of π-graphs processes.The whole framework has been implemented during the course of this thesis. Our prototype tool provides a simulator for π-graphs models. These models can also be compiled into high-level Petri nets and then manipulated using the SNAKES framework. Finally, we provide an encoding of open system logic into linear temporal logic with state properties to be used with the NECO model checker for the automated verification of properties. Thanks to the bidirectional encoding from-and-to high-level Petri nets, counterexamples provided by the model checker for Petri nets can be easily reconstructed in terms of the original π-graphs.