Verification paramétrée de systemes distribues dynamiques – PaVeDyS

Ce projet vise le développement des méthodes formelles de vérification pour systèmes distribues avec un nombre non-borne de participants, dans lesquelles la communication s'effectue a travers un reseau reconfigurable ou mobile. En plus des propriétés de correction classiques dans la théorie du parallélisme, tels l'absence de blocages et des violations de régions critiques, nous considérons aussi la convergence et l'auto-stabilisation. Le projet est structure en trois axes. La première axe vise a développer des modelés pour des systèmes distribues, tout en capturant les aspects essentiels, tels la reconfiguration dynamique et la mobilité. Les modelés seront définis utilisant des combinaisons des logiques avec la théorie des automates et celle des jeux, avec des aspects stochastiques, permettant l’étude des propriétés algorithmique et des classes de complexité pour les problèmes de vérification considères. La seconde axe vise a trouver des (semi-)algorithmes capables d'analyser certaines classes de systèmes distribues. La troisième axe consiste a appliquer les (semi-)algorithmes de vérification aux protocoles distribues connus et souvent implémentes dans la pratique (élection, consensus, couverture, routage, etc.). Ces algorithmes distribues sont a présent un défi pour les méthodes existantes de vérification de logiciel, qui s'appliquent principalement aux programmes concurrents avec de la mémoire partagée.