Thèse en cours
Equipe :
Contribution à la modélisation formelle d'essaim de robots mobiles
Début le 01/10/2016
Direction : CONTEJEAN, Evelyne
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI - VALS
Soutenue le 18/12/2020 devant le jury composé de :
Rapporteurs :
- David Ilcinkas, Chargé de recherche, Université de Bordeaux
- Micaela Mayero, Maître de conférences, Université Paris 13
Examinateurs :
- Quentin Bramas, Maître de conférences, Université de Strasbourg
- Isabelle Guérin Lassous, Professeure, Université Claude Bernard Lyon 1
- Pascale LeGall, Professeure, Université Paris Saclay
- Xavier Urbain, Professeur, Université Claude Bernard Lyon 1
Directrice :
- Évelyne Contejean, Directrice de recherche, CNRS
Co-Encadrant :
- Thibaut Balabonski, Maître de conférences, Université Paris Saclay
Invités :
- Lionel Rieg, Maître de conférences, ENSIMAG
- Sébastien Tixeuil, Professeur, Sorbonne Université
Activités de recherche :
Résumé :
L’algorithmique distribuée fait partie des domaines où le raisonnement informel n’est pas une option, en particulier lorsque des erreurs dites byzantines peuvent survenir. Elle est également caractérisée par une grande diversité de modèles dont les modulations subtiles impliquent des propriétés radicalement différentes. Nous nous intéressons aux « réseaux de robots » : nuages d’entités autonomes devant accomplir une tâche en coopération. Les applications que laissent envisager ces essaims d’agents sont extrêmement prometteuses : exploration et recherche de survivants dans des zones dévastées, patrouilles et vols de drones en formation, etc. Ces quelques exemples potentiellement critiques soulignent la grande dynamicité du modèle; ils indiquent également à quel point des défaillances des robots ou des erreurs dans les protocoles distribués qui les équipent peuvent avoir de désastreuses conséquences.
Pour garantir la sûreté des protocoles et la sécurité des tâches, nous visons à l’obtention, à l’aide de l’assistant à la preuve Coq, de validations mécaniques formelles de propriétés de certains protocoles distribués. Un prototype de modèle formel Coq pour les réseaux de robots, Pactole, a récemment montré la faisabilité d’une approche de vérification par assistant à la preuve dans ce cadre. Il capture assez naturellement de nombreuses variantes de ces réseaux, notamment en ce qui concerne la topologie ou les propriétés des démons. Ce modèle est bien sûr à l’ordre supérieur et s’appuie sur des types coinductifs. Il permet de démontrer en Coq à la fois des propriétés positives : le programme embarqué permet de réaliser la tâche quelle que soit la configuration de départ, comme des propriétés négatives : il n’existe aucun programme embarqué permettant de réaliser la tâche.
Dans le cadre émergent des réseaux de robots, les modèles sont distingués par les caractéristiques et capacités des robots, la topologie de l’espace dans lequel ils évoluent, le degré de synchronisme (modélisé par les propriétés du démon d’activation), les erreurs pouvant survenir, etc. Le prototype Pactole n’exprime que certaines de ces variantes. Pensé dans un cadre théorique (robots ponctuels, déplacements instantanés, etc.), des hypothèses restent hors de sa portée, en particulier des hypothèses réalistes comme des exécutions totalement asynchrones ou des risques de collision. L’absence de collision est fondamentale dans toutes les applications liées aux évolutions en formation (drones) et une condition de sécurité critique dès qu’on s’intéresse au transport aérien. Une validation formelle de cette propriété revêt donc une grande importance.
Le travail consiste à étendre le modèle formel afin de prendre en compte des évolutions asynchrones de robots volumineux. Cette modélisation doit permettre une formulation aisée de protocoles et des tâches qu’ils sont censés réaliser. On s’intéressera en particulier à garantir l’absence de collision au cours de déplacements potentiellement complexes.
