L’algorithmique distribuée et les systèmes distribués en général forment un domaine où le raisonnement informel n’est pas une option. Un problème à l'étude dans un cadre distribué, avec ou sans défaillances est extraordinairement sensible aux altérations des hypothèses. Une approximation mineure un léger décalage de modèle peuvent avoir des conséquences catastrophiques une fois le système déployé. Malgré tout le soin apporté par leurs auteurs on trouve encore régulièrement des articles comportant des erreurs, même lorsqu'ils sont publiés dans des revues prestigieuses.

Nous nous intéressons aux méthodes formelles pour assurer la correction des protocoles distribués et obtenir des garanties sur les résultats théoriques. Parmi celles-ci nous nous concentrons sur la preuve formelle, c'est-à-dire la preuve vérifiée mécaniquement par un assistant à la preuve. Ces assistants bénéficient d'un grand pouvoir d'expression, ils permettent de certifier comme correctes des preuves de correction comme des preuves d'impossibiité. À la différence des model-checkers complètement automatisés, ils offrent une plus grande généralité d'utilisation, n'étant pas limités à des instances de problèmes. L'expressivité a un coût : s'appuyant sur des logiques non décidables, les assistants à la preuve sont interactifs et requièrent une expertise certaine de la part de l'utilisateur, ce qui est un frein à leur large utilisation.

L'objectif de cette thèse est d'offir des moyens d'automatisation afin de décharger les utilisateurs de tâches techniques ou fastidieuses au cours de leurs développements formels ; ses résultats contribueront donc à la diffusion des approches par preuve formelle pour le développement de protocoles distribués sûrs. Plus précisément dans le cadre du projet ANR SAPPORO est développé un cadre formel pour protocoles distribués, Pactole, destiné à l'assistant à la preuve Coq. Ce cadre comprend une bibliothèque importante de définitions, lemmes et études de cas. Il ne dispose que de très peu d'automatisation et il est important de l'en équipper.

Deux niveaux d'automatisation sont abordés.

Le premier niveau concerne le cas particulier de la modélisation de calcul locaux.  Outil théorique et pratique puissant pour l’étude de calculs distribués dans un graphe : les calculs locaux vérifient de bonnes propriétés pour la compréhension, l’étude et l’analyse des systèmes distribués. Ils sont en effet suffisamment intuitifs pour permettre le développement de programmes et complètement formels, autorisant ainsi une démarche de certification.  On peut les représenter par des réseaux de processeurs n’ayant accès qu’à des ressources locales, c’est-à-dire les états des voisins et des canaux qui y mènent.  Le comportement d’un algorithme est donc déterminé par l’état initial du réseau, ses propriétés locales et globales, et enfin les primitives de communication. Les calculs locaux sont en fait des systèmes d’interactions locales. Parmi ces modèles, les systèmes de récriture de graphes étiquetés de Litovsky, Métivier et Mosbah bénéficient du haut niveau d’abstraction apporté par la récriture et ont permis l’obtention d’importants résultats (par exemple un algorithme d’élection de leader totalement asynchrone ne nécessitant que des messages de taille polynomiale).  Une première étape concerne l’expression et l’analyse, en termes de récritures (de graphes puis de termes), des notions pertinentes pour des agents distribués dans un réseau. À des fins d’automatisation, une partie de ces traductions sera implantée dans une boîte à outils logicielle pour systèmes de récriture. On étudiera alors les systèmes produits afin de développer des techniques automatiques de preuve de propriété (par exemple de type terminaison/stabilisation) : des topologies particulières de graphes (grilles, anneaux, structures régulières) peuvent en effet caractériser des fragments (semi-)décidables et permettre le développement de techniques s'inspirant d'approches de preuve automatique sur les termes.

Le second niveau concerne la définition de tactiques de preuve de haut niveau, aussi génériques que possible, afin de réduire significativement la taille des développements et de faciliter leur lecture. Deux pistes seront étudiées : le développement en LTAC, d'une part, qui offre les moyens de composer rapidement et facilement des tactiques, le développement directement en OCAML, d'autre part, solution plus lourde mais offrant davantage de puissance. Un objectif attendu dans ce contexte est une facilitation du traitement des cas des exécutions asynchrones et des développments de protocoles probabilistes.