Auto-stabilisation et amélioration de la sûreté dans les environnements distribués évoluant dans le temps – ESTATE

La disponibilité de moyens de communiquer sans fil a énormément augmenté ces dernières années. Cette évolution apporte de nouveaux usages, et avec elle une multitude de problèmes pratiques et théoriques. Elle oblige à concevoir de nouvelles applications pour permettre aux entités (agents, terminaux) d'interagir, la plupart du temps, de manière autonome.
Ce nouveau paradigme de systèmes distribués, appelé informatique ubiquitaire, conduit à des changements significatifs dans l'ingénierie des télécommunications qui doivent pouvoir s'adapter à des changements importants dans le graphe de communication, principalement dûs à la mobilité des agents communicants. La dynamique de ces systèmes distribués a un impact significatif sur la nature des tâches qui peuvent être exécutées. La conception d'applications au dessus de ce type de réseaux nécessite de s'adapter aux changements topologiques et au manque de structures logiques fixes habituelles telles que les arbres, les spanners, les ensembles dominants minimaux, la présence d'un leader, etc.
Le projet ESTATE consiste à poser les bases d'une algorithmique pour l'informatique autonome dans les systèmes distribués et réseaux fortement dynamiques. En d'autres termes, nous avons l'intention de concevoir un modèle doté des bases algorithmiques nécessaires à l'émergence de capacités d'autonomies, par exemple, l'auto-organisation, l'auto-guérison, auto-configuration, auto-management, l'auto-optimisation, l'auto-adaptabilité, l'auto-réparation, etc.

Pour ce faire, nous envisageons trois grands axes de recherche:

- Le premier consiste à travailler sur les fondements théoriques de l'informatique autonome dans les systèmes dynamiques. Nous envisageons notamment de considérer l'autostabilisation comme une approche concrète à la mise en oeuvre d'une algorithmique distribuée fondatrice de l'informatique autonome.

- Le second vise à renforcer la sécurité dans certains cas. Nous prévoyons de revoir certaines variantes renforçant la sûreté d'algorithmes auto-stabilisants dans le contexte dynamiques. Nous envisageons d'établir les conditions minimales en termes de niveau de dynamique pour permettre d'avoir un niveau de sûreté donné.

- Le troisième axe devra fournir des garanties formelles supplémentaires en proposant un cadre de preuves formelles basé sur l'assistant de preuves Coq. Ce dernier permettra de construire (semi-)automatiquement des preuves certifiées, à la fois pour les deux premiers axes. Pour cela, nous devrons identifier une formalisation adéquate et des schémas généraux de preuves destinés à montrer la correction des algorithmes.

Les trois axes interagiront entre eux de la manière suivantes : le premier apportera des bornes inférieures et des limitations au second, qui en retour devra fournir des cas d'utilisation au premier. Le troisième axe apportera des preuves certifiées aux résultats obtenus dans les deux premiers axes, par exemple, des résultats d'impossibilité, des bornes de complexités, des preuves de justesse d'algorithmes distribués. Les algorithmes fournis par les deux premiers axes seront validés selon quatre approches complémentaires : (i) la preuve "à-la-main" classique, (ii) la preuve certifiées (semi-)automatique fournie par le troisième axe, (iii) par simulations et (iv) dans un contexte mobile réel. Les deux dernières approches seront implantées sur des plateformes dédiées.