Auteur
Boukala, Mohamed Cherif
Directeur de thèse
Mokhtari, A. (Professeur)
Filière
Informatique
Diplôme
Doctorat
Titre
Vérification distribuée des systèmes complexes.
Mots clés
Espace des états, Méthodes de l' ; Petri, Réseaux de ; Théorèmes : Démonstration automatique ; Logique temporelle ; Systèmes, Analyse de
Résumé
Afin de pallier au problème de l’explosion combinatoire dont souffre les méthodes de vérification formelles, en particulier celles basées sur les modèles, plusieurs techniques ont été proposées. Nous nous sommes intéresse dans cette thèse à l’approche basées sur la distribution. En effet, le fait de faire coopérer plusieurs stations permet d’offrir un espace mémoire et une puissance de calcul très importants, et peut permettre l’analyse de systèmes qui n’auraient jamais pu l’être sur une seule machine. L’idée consiste alors à répartir l’espace d’états sur les différentes stations et d’adapter les algorithmes de vérification à ce nouveau contexte. Dans la première partie de notre travail nous nous somme intéresse à la génération distribué de l’espace d’états et aux problèmes inherents à celle-ci : équilibre de charges, réduction du temps d’oisiveté des processeurs, minimisation du nombre de messages échangés . . . . Nous avons proposé un certain nombre de solutions pour permettre de remédier à ces problèmes. Le choix d’une bonne fonction de hashage est déterminant, regroupement des messages, granularité . . . Dans une seconde étape, nous nous sommes interessé au proprités dites générales : atteignabilité, vivacité, états d’accueil). Pour la première proporiété on obtient de très bon résutats avec une acceleration super-lineaire. La deuxième et la troisième propriété nécessitent la construction de toutes les composantes fortement connexes de l’espace, donc un nombre important d’échange de messages, mais permet néanmoins d’analyser des problèmes de taille importante. Nous nous somme aussi interessé à la vérification de propriétés par le modèl-checking, nous avons axé notre travail sur la model-checking de CTL. Nous avons donné la démarche permettant de distribuer ces algorithmes et proposé de déterminer en distribué le ou les contre-exemples lorsque la propriété vérifiée n’est pas vraie. Des prototypes ont été réaliser afin de mener des tests des algorithmes proposés. Quand au model-checking de LTL nous nous sommes contenté de donner une proposition qui permettrait d’améliorer le recherche de cycles dans l’espace d’états. Enfin, nous avons proposé une nouvelle approche de distribution de la vérification basée sur la modularité. Ainsi, Chaque module du système est assigné à un processus client qui construit les graphes dits internes, le processus coordinateur construit le graphe de synchronisation. Les algorithmes de vérification de l’atteignabilité, d’existence d’états bloquants, de la vivacité et d'états d’accueil ont été aussi adaptés pour l’approche distribuée. La conjugaison des approches modulaires et l’approche distribuée ont permis d’obtenir des de très bons resultats, en particulier lorsqu’on à un système faiblement couplé. Ainsi, pour le problème des philosophes par exemple nous avons pu générer l’espace d’états d’un problème dont la taille normale est de plus de 6.1023 .
Date de soutenance
08/07/2012
Cote
004.24
Pagination
104 p.
Illusatration
ill.
Format
30 cm.
Notes
Support papier accompagné d'un CD-Rom ; Bibliogr. p. 99-104
Statut
Traitée