Modelling and analysing open reconfigurable systems
Viet Van Pham · 2014
Modélisation et analyse des systèmes ouverts reconfigurables 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.