Vérification efficace de programmes distribués asynchrones

Publié le
Equipe
Date de début de thèse (si connue)
dès que possible
Lieu
Rennes
Unité de recherche
IRISA - UMR 6074
Description du sujet de la thèse

Le model checking est une méthode formelle de vérification des systèmes informatiques basée sur l’exploration exhaustive de toutes les évolutions possibles d’un modèle du système à vérifier. Cette méthode est plus facile à utiliser qu’un assistant de preuve, qui demande à l’utilisateur d’inventer des objectifs intermédiaires quand l’objectif initial est hors de portée. La vérification formelle de logiciels (software model checking) vise à utiliser les méthodes de model checking d'exploration exhaustive directement sur un logiciel à vérifier, sans modélisation préalable. Cela laisse envisager des outils entièrement automatiques, capables de démontrer formellement des propriétés sur des programmes sans intervention de l’utilisateur, en testant de manière exhaustive les exécutions possibles du programme. L'objectif de cette thèse est d’étendre un outil existant dans nos équipes.

Le premier axe de travail d’ordre algorithmique, pour répondre à l’explosion combinatoire qui résulte de l’exploration exhaustive de l’espace d’états du système: le graphe d’états d’un ensemble fini de processus séquentiels finis exécutés en parallèle est de taille exponentielle par rapport à la taille de chaque processus. Cela rend souvent impossible en pratique l’exploration de systèmes réels même de taille modérée. De nombreuses techniques de réduction de cet espace d’états ont été proposées dans la littérature, en exploitant par exemple des propriétés de redondance ou de symétrie. L’approche proposée dans cette thèse vise à ajouter des stratégies de guidage en plus de ces techniques. Il s’agit d’explorer en priorité les parties de l’espace d’états réduit où se trouvent probablement les éventuels bugs cherchés.

Le travail envisagé n’est cependant pas seulement algorithmique, et nous souhaitons continuer nos travaux techniques afin d’améliorer la qualité logicielle de l’outil, en nous appuyant entre autres sur des travaux antérieurs de génie logiciel et qualité logicielle dans le domaine des outils de software model checking. L’objectif à terme est de réaliser un outil pratique permettant aux analystes non spécialistes des méthodes formelles de vérifier formellement des applications réelles distribuées asynchrones.

Bibliographie

[CACM11] Formal Analysis of MPI-Based Parallel Programs, Gopalakrishnan et Al. Communication of the ACM, 2011.
https://cacm.acm.org/magazines/2011/12/142546-formal-analysis-of-mpi-ba…

[McSimGrid17] Verifying MPI Applications with Mc SimGrid, T. A. Pham, T. Jéron, M. Quinson. Workshop on Software Correctness for HPC Applications (Correctness'17)
https://hal.inria.fr/hal-01632421

[DPOR] Model checking for programming languages using VeriSoft, Patrice Godefroid - ACM Symposium on Principles of Programming Languages (POPL'97).
https://www.ccs.neu.edu/home/wahl/Teaching/Software-Model-Checking/2016…

[ODPOR] Optimal dynamic partial order reduction, Abdulla, Aronis, Jonsson, Sagonas - ACM Symposium on Principles of Programming Languages (POPL'14).
https://user.it.uu.se/~bengt/Papers/Full/popl14.pdf

[UPDOR] Unfolding-based partial order reduction, Rodriguez, Sousa, Sharma, Kroening - 26th International Conference on Concurrency Theory (CONCUR’15).
https://arxiv.org/pdf/1507.00980.pdf

[MBI] The MPI BUGS INITIATIVE: a Framework for MPI Verification Tools Evaluation. M. Laurent, E. Saillard, M. Quinson. Workshop on Software Correctness for HPC
Applications (Correctness'21). https://hal.archives-ouvertes.fr/hal-03474762

[Pham19] Unfolding-based Dynamic Partial Order Reduction of Asynchronous Distributed Programs, Pham, Jéron, Quinson. 39th International Conference on Formal Techniques for Distributed Objec
ts, Components, and Systems (FORTE'19) https://hal.inria.fr/hal-02109769/document

[DirecteMC] Survey on Directed Model Checking, S. Edelkamp, V. Schuppan, D. Bošnački, A. Wijs, A. Fehnker, H. Aljazzar. Workshop on Model Checking and Artificial
Intelligence (MoChArt'08). https://link.springer.com/chapter/10.1007/978-3-642-00431-5_5


 

Liste des encadrants et encadrantes de thèse

Nom, Prénom
Martin Quinson
Type d'encadrement
Directeur.trice de thèse
Unité de recherche
irisa
Equipe

Nom, Prénom
Thierry Jéron
Type d'encadrement
Directeur.trice de thèse
Unité de recherche
IRISA
Equipe
Contact·s
Nom
Martin Quinson
Email
martin.quinson@ens-rennes.fr
Mots-clés
model-checking, systèmes distribués, recherche de bug