Méthodes formelles pour la conception d'algorithmes distribués – FREDDA

De part l'ubiquité des algorithmes distribués dans les systèmes informatiques actuels, il est important de concevoir des solutions algorithmiques robustes et adaptables, qui peuvent être déployées dans des applications à grande échelle. Ces dernières années, les chercheurs en systèmes distribués ont développé des techniques élaborées pour la conception et l'analyse d'algorithmes distribués. Un point clef dans le développement de ces algorithmes sont les hypothèses spécifiques considérées sur le contexte d'exécution. Par exemple, la communication peut être synchrone ou asynchrone, les entités dans le réseau peuvent être ou non munies d'un identificateur unique ou encore un certain nombre d'erreurs et de pannes peuvent avoir lieu pendant une exécution. Ces hypothèses sont cruciales et peuvent mener à différentes familles d'algorithmes conçues pour un contexte spécifique. Bien qu'il y aient de nombreuses techniques pour la conception et l'analyse d'algorithmes, la plupart des algorithmes existant restent confinés à un modèle d'exécution très spécifique et il est difficile d'en obtenir un nouvel algorithme pour un modèle différent. De plus les preuves de correction des algorithmes distribués sont souvent très complexes. Cela est du en partie au fait qu'ils sont souvent conçus pour un nombre non borné de participants et qu'ils peuvent utiliser des ressources dont la quantité dépend de ce dernier nombre. Pour finir, leur preuve de correction dépend aussi fortement du contexte d'exécution et elles sont elles-aussi difficilement adaptables à des variations. En d'autres termes, les algorithmes distribués ont tendance à ne pas être robustes.

Le but de notre projet est de développer des méthodes formelles pour fournir une aide algorithmique pour la conception d'algorithmes distribués robustes. La robustesse d'algorithmes distribués est un problème difficile qui n'a jusqu'à présent pas été beaucoup considéré et il n'y a pas de méthodes systématiques pour garantir ou vérifier le comportement d'un algorithme plongé dans un contexte d'exécution différent de celui pour lequel il a été conçu.Nous proposons de concevoir des techniques automatiques s'appuyant sur les méthodes formelles pour vérifier la robustesse d'algorithmes distribués et pour aider le développement d'applications robustes. Nous aurons deux types méthodes: statique, basée sur les techniques classiques de vérification, et dynamique, par la synthèse de moniteurs distribués dont le rôle est de vérifier à l'exécution la correction ou la validité des hypothèses sur le contexte.

Les méthodes et outils que nous proposerons pour réaliser l'analyse de robustesse seront intégrés dans un cycle de développement dont le rôle sera de construire un algorithme robuste à partir d'un algorithme correct dans un certain contexte. Ce cycle fonctionnera de la façon suivante : tout d'abord, il testera si l'algorithme est correct dans le nouveau contexte d'exécution, dans le cas positif, nous obtenons un algorithme robuste, dans le cas négatif, notre analyse produit un contre-exemple pour la robustesse qui peut être utilisé par des experts en systèmes distribués pour modifier l'algorithme et éliminer ainsi les comportements non robustes. Après un certain nombre d'itérations d'un tel cycle, nous obtenons un algorithme qui est plus robuste que l'algorithme d'origine.

Afin de développer des méthodes pour analyser la robustesse d'algorithmes distribués, nous avons regroupé des chercheurs venant à la fois de la communauté de systèmes distribués et de celle des méthodes formelles. Nous avons des experts dans deux domaines de recherche complémentaires. D'un côté, nous avons la communauté des systèmes distribués avec leur savoir faire pour établir la correction d'algorithmes distribués en utilisant des techniques ad-hoc qui dépendent fortement du contexte d'exécution. Et de l'autre côté, la communauté d'experts en vérification qui fournit des modèles formels et des techniques d'analyses automatiques.