Ce projet de recherche doctorale est publié a été réalisé par Fabrice Kordon

Description d'un projet de recherche doctoral

Exploitation des symétries pour le model checking de systèmes répartis : du modèle au codage

Mots clés :

Résumé du projet de recherche (Langue 1)

{{{Equipe d’accueil}}} La thèse se déroule au sein de l’équipe MoVe (Modélisation et Vérification) au sein du département "Réseaux et systèmes répartis" du laboratoire LIP6. Cette équipe se compose actuellement de 22 enseignants-chercheurs permanents (dont 9 habilités à diriger des recherches) et 10 doctorants. L’équipe MoVe s’intéresse à la modélisation et à l’analyse des systèmes répartis à composants interopérables. Son objectif est de développer des techniques de modélisation, des outils de vérification et des générateurs de programmes permettant à des ingénieurs de développer sans risque des applications réparties complexes. Les tech- niques et outils développés se placent dans le contexte d’une approche MDD (Model Driven Development). {{{1 Introduction}}} L’évolution des technologies de communication a accru l’utilisation de systèmes répartis dans de nombreux secteurs d’activité : industries, administrations, applications grand public... En particulier, les domaines critiques sont de plus en plus concernés : transports, applications médicales ({life critical}), militaires, spatiales ({mission critical}), mais aussi commerciales ou industrielles ({business critical}). La criticité de ces domaines nécessite de garantir le fonctionnement des systèmes en question, et renforce l’intérêt d’une étape de vérification formelle dans le cycle de développement des produits. La modélisation et la vérification constituent d’une part une assistance à la conception, par le formalisme qu’elles offrent, et d’autre part permettent un haut degré de fiabilité des systèmes développés. Les systèmes répartis, dont l’utilisation se répand tout en requérant de plus en plus de fiabilité, sont une cible de choix pour ces techniques. Pour toutes ces raisons, la demande d’outils de modélisation et de vérification est aujourd’hui en forte croissance. Cette demande et le manque de maturité des outils actuels font de la vérification un champ de recherches actif. {{{2 Contexte scientifique}}} Le model checking est l’une des principales approches de vérification. Il repose sur l’élaboration d’un modèle du système à vérifier, sur lequel sont énoncées les propriétés à prouver (à l’aide d’une logique appropriée). Ces propriétés sont vérifiées par l’exploration exhaustive des évolutions possibles du modèle (l’espace d’états). La génération et le parcours de l’espace d’états sont facilement automatisables, mais les algorithmes naïfs sont victimes de l’explosion combinatoire du nombre d’états dès que les modèles deviennent réalistes. La mise en œuvre pratique de l’automatisation requiert donc l’utilisation de différentes techniques d’optimisation. Deux axes sont à considérer : -* l’exploitation des symétries du système([1]),pour construire des états symboliques représentant des familles d’états concrets aux propriétés communes. Cette notion est à l’origine de la théorie des Symmetric Nets (SN), variante des Coloured Petri Nets ([2],[3]) -* l’utilisation de techniques de codage et de compression, grâce à l’emploi de diagrammes de décision notamment, pour optimiser la charge de la mémoire ([4]). Ces deux techniques très différentes peuvent être considérées de manière indépendante. Elles n’en sont pas moins complémentaires, et particulièrement intéressantes dans la perspective d’une implémentation. La première suppose une réflexion au niveau des formalimes utilisés, pour repérer les symétries du système, qui peuvent aboutir à des redondances d’information. Les états symétriques du système sont regroupés au sein de classes d’équivalence d’états, réduisant ainsi l’espace d’états à explorer. La seconde approche est essentiellement algorithmique, et repose sur l’optimisation du codage et de l’utilisation de la mémoire. Elle s’appuie sur l’utilisation de diagrammes de décision pour coder les états. Le travail de thèse s’insère également dans les efforts de l’équipe MoVe pour combattre le problème de l’explosion combinatoire. Des travaux ont déjà été menés ces dernières années au sein de l’équipe. Certains concernent l’exploitation des symétries : détection des symétries, symétries structurelles, symétries globales et locales... D’autres se sont concentrés sur l’algorithmique nécessaire à l’exploration d’un espace d’états : équivalence et traduction entre différents formalismes (colorés - P/T), codages exploitant les différents niveaux de symétrie, codages hiérarchiques... MoVe se distingue notamment par deux idées originales : -* l’étude des symétries partielles et locales ([5],[6],[7]) -* les diagrammes de décision hiérarchiques ([8]). L’équipe intègre ses outils de modélisation et vérification des réseaux de Petri au sein de sa plateforme FrameKit. Ce dispositif oriente l’équipe vers un souci de faisablilité : les nouveaux concepts conduisent à la réalisation de prototypes qui peuvent être confrontés à des études de cas. {{{3 Problématique}}} La thèse vise à approfondir les travaux résumés par [9] menés au sein de l’équipe : la génération de l’espace d’états d’un SN en utilisant un codage en Data Decision Diagrams (DDD). Ceux-ci étendent les Binary Decision Diagrams (BDD) en autorisant la valuation des arcs avec des entiers. Ils introduisent également les homomorphismes, outils de manipulation souples et puissants ([10]). Plus précisément, le travail se focalise sur deux principaux axes : -* établir un cadre général pour l’exploitation des symétries structurelles d’un modèle. Cette réification doit permettre de dissocier la symétrie d’un formalisme particulier. -* approfondir les techniques de codage et d’optimisation de la mémoire, notamment en attachant un codage à chaque niveau de symétrie identifié dans le processus de réification. Sont donc conduites en parallèle la réflexion sur les modèles et celle sur leurs codages. Ainsi, l’optimisation de l’utilisation mémoire est affinée : les codages aux différents niveaux de symétrie peuvent évoluer indépendamment, pour exploiter au mieux les différents types de contraintes. {{L’exploitation des symétries structurelles}} Le processus de réification vise en premier lieu l’identification des caractéristiques de la symétrie d’un modèle indépendamment du formalisme. Il doit donc permettre de valider simplement le caractère symétrique de nouveaux formalismes. Mais il doit aller plus loin : identifier différents niveaux de symétries, correspondant à des classes de formalismes, chaque niveau étant caractérisé indépendamment des formalismes. {{Optimisation de l’utilisation de la mémoire}} L’intérêt des symétries est l’impact qu’elles ont sur la représentation en mémoire. La symétrie induit en effet une contrainte qu’il n’est pas nécessaire de reproduire dans le codage. L’identification de différents niveaux de symétries pour les modèles va donc naturellement de pair avec la définition d’un codage pour chaque niveau, exploitant au mieux les particularités du niveau en question. On aboutit donc à un codage variable, dépendant du degré de symétrie du modèle. On envisage d’aller plus loin, en utilisant un codage dynamique : pour un même modèle, le codage dépend de la position dans l’espace d’état. Les modèles peuvent en effet présenter localement des symétries plus ou moins fortes. L’idée est de ne pas niveler la symétrie globale par le bas. La mise en place de codages dynamiques peut être facilitée par l’utilisation de PolyDD, diagrammes de décision polymorphes ([11]), afin de garantir la cohérence d’un codage même dynamique. Enfin, la réflexion en parallèle sur les formalismes et les codages doit permettre de mieux comprendre les interactions entre les deux techniques. Elle mettra en lumière d’éventuels effets symbiotiques, positifs ou négatifs, pour une meilleure compréhension des relations entre formalismes et codages. {{{4 Démarche}}} Le travail de thèse s’appuie sur le formalisme des Symmetric Nets with Bags (SNB), variante des SN dans laquelle les pt pas la symétrie, et ne bride pas les performances de la vérification. Le travail de thèse débute par l’étude de ces SNB, en tant que cas particulier devant conduire au processus de réification évoqué plus haut. Cette démarche aura été initiée en stage de M2, à travers l’implémentation d’un générateur de l’espace d’états d’un SN, en utilisant des Hierarchical Set Decision Diagrams (SDD) comme base de codage. Ceux-ci, introduits dans [8], sont des diagrammes de décision hiérarchiques, et vont plus loin que les DDD. Ce prélude aura permis au candidat de se familiariser avec le sujet, et d’amorcer sa reflexion, sur les codages notamment, et le lien entre symétries et représentations. Le travail devrait ensuite suivre les étapes suivantes : -* l’identification de différents types de symétries, et des caractéristiques d’un formalisme propices à leur exploitation -* la détermination de codages pour représenter ces symétries, débouchant sur un codage dynamique des états. À ce stade, le processus de réification est achevé, et il conviendrait de le synthétiser au sein d’un formalisme reflétant les niveaux de symétrie identifiés. Ce formalisme pourra être utilisé pour en réécrire d’autres déjà existants afin d’en exhiber les symétries structurelles, mais aussi pour définir de manière générique de nouveaux formalisme à partir d’un degré de symétrie souhaité. Le travail de thèse pourra s’achever par l’implémentation d’un outil de vérification automatique reprenant ce formalisme et exploitant les codages variables, voire dynamiques, évoqués plus haut. La réflexion sur les symétries s’appuiera sans doute sur l’expérience de MoVe en matière de symétries partielles ([6],[7]). De même, la détermination de "bons" codages devra s’appuyer sur les précédentes réalisations ([9]). {{{Références}}} [1] T. Junttila. {On the Symmetry Reduction Method for Petri Nets and Similar Formalisms}. Research report, Espoo, Finland, September 2003. [2] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. {Stochastic well-formed colored nets and symmetric modeling applications}. IEEE Transactions on Computers, 42(11) :1343–1360, 1993. [3] K. Jensen. {Coloured petri nets}. Petri nets : central models and their properties, pages 248–299, 1992. [4] J.R. Burch, E.M. Clarke, et al. {Symbolic model checking : 10^20 States and beyond}. Information and computation, 98(2) :142–170, 1992. [5] E. Allen Emerson and Richard J. Trefler. {From asymmetry to full symmetry : New techniques for symmetry reduction in model checking}. In In Conference on Correct Hardware Design and Verification Methods, pages 142–156. Springer, 1999. [6] Serge Haddad, Jean-Michel Ilié, and Khalil Ajami. {A model checking method for partially symmetric systems}. In Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), FORTE/PSTV 2000, pages 121–136, Deventer, The Netherlands, The Netherlands, 2000. Kluwer, B.V. [7] Souheib Baarir and Alexandre Duret-Lutz. {Emptiness check of powerset buchi automata using inclusion tests}. In Proceedings of the Seventh International Conference on Application of Concurrency to System Design, pages 41–50, Washington, DC, USA, 2007. IEEE Computer Society. [8] J.M. Couvreur and Y. Thierry-Mieg. {Hierarchical decision diagrams to exploit model structure}. Lecture notes in computer science, 3731 :443, 2005. [9] Y. Thierry-Mieg, J.M. Ilié, and D. Poitrenaud. {A symbolic symbolic state space representation}. Formal Techniques for Networked and Distributed Systems–FORTE 2004, pages 276–291, 2004. [10] J.M. Couvreur, E. Encrenaz, E. Paviot-Adet, D. Poitrenaud, and P.A. Wacrenier. {Data decision diagrams for Petri net analysis}. Application and Theory of Petri Nets 2002, pages 129–158, 2002. [11] A. Linard, E. Paviot-Adet, F. Kordon, D. Buchs, and S. Charron. {polyDD : Towards a Framework Generalizing Decision Diagrams}. In 10th International Conference on Application of Concurrency to System Design (ACSD’2010), pages 124–133, Braga, Portugal, June 2010. IEEE Computer Society.