Description
Date depot: 1 janvier 1900
Titre: Exploitation des symétries pour le model checking de systèmes répartis : du modèle au codage
Directeur de thèse:
Fabrice KORDON (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
{{{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 condu
Doctorant.e: Colange Maximilien