Vérification Formelle de Composants Distribués – PiCoq

L'utilisation croissante de systèmes informatiques rend nécessaire une analyse
rigoureuse de leurs propriétés, pour spécifier et prouver des garanties sur
leurs comportements. De nombreux systèmes étant distribués ou reconfigurables,
leur complexité les rend quasiment impossibles à analyser directement, que ce
soit à la main ou avec des outils d'analyse automatique.

La recherche en théorie de la concurrence et en algèbres de processus a
produit des modèles formels décrivant de nombreux aspects de la programmation
distribuée, comme les communications d'ordre supérieur, la mobilité de code ou
la mise à jour de composants. Des théories comportementales ont aussi été
développées afin de spécifier et prouver correct le comportement de ces
systèmes. Beaucoup de travail reste cependant nécessaire pour les rendre
utilisables en pratique.

Par ailleurs, le besoin d'obtenir des garanties rigoureuses justifie
l'utilisation de méthodes formelles, pour certifier le comportement de ces
systèmes. Jusqu'à récemment, les preuves certifiées par assistant de preuve
n'étaient envisageables que dans des cas assez simples. Cependant, des travaux
récents ont montré que les assistants de preuve sont assez mûrs pour être
utilisés dans des cas plus conséquents, que ce soit dans le domaine des
mathématiques ou de la sémantique des langages de programmation (c.f. la
preuve du théorème des 4 couleurs par Gonthier et Werner ou le compilateur
certifié développé dans le cadre du projet ANR Compcert). Néanmoins, ces
progrès concernent les langages séquentiels; les outils pour raisonner sur des
systèmes concurrents et distribués avec un assistant de preuve n'existent pas
encore.

Nous proposons donc dans le projet PiCoq de développer un environnement pour
la vérification formelle de propriétés de programmes distribués à composants.
Notre approche se situe à l'interface entre deux domaines de recherche: la
théorie de la concurrence et les assistants de preuve.

Notre but dépend de trois avancées scientifiques.

1. Trouver un cadre mathématique facilitant l'analyse modulaire de systèmes
concurrents et distribués. A cause de leur grande taille et de leurs
interactions complexes, ces systèmes ne peuvent pas être analysés globalement.
Ils doivent être décomposés en éléments dont le comportement individuel peut
être compris.

2. Améliorer les techniques de preuves pour les systèmes modulaires et
distribués. Bien que les techniques comportementales sont bien comprises pour
les systèmes du premier ordre, ce n'est pas le cas pour ceux d'ordre
supérieur. Nous avons également besoin de généraliser les approches modulaires
afin d'éviter les redondances dans les preuves et ainsi faciliter
l'utilisation d'assistants.

3. Définir un calcul de processus minimal fidèle aux idiomes de la
programmation distribuée à composants mais pour lequel des propriétés
fondamentales d'équivalence comportementale peuvent être montrées. Cette
avancée est intimement liée à la précédente: les techniques de preuves
adaptées à un calcul dépendent fortement des propriétés d'équivalence
comportementale de ses primitives.

Au delà de ces avancés théoriques, le développement de l'environnement
lui-même présente un défi. Ce développement requière des techniques de preuves
sophistiquées pour par exemple gérer les lieurs, implémenter des tactiques
pour résoudre automatiquement des propositions décidables ou utiliser
intelligemment des modules pour rendre le code lisible et réutilisable.

Finalement, nous validerons notre approche en certifiant dans notre
environnement des preuves portant sur des systèmes distribués, dont la
formalisation d'articles classiques ou récents, la spécification formelle d'un
calcul de processus pour la modélisation d'un modèle à composants et la preuve
de correction d'une machine abstraite distribuée.