Sûreté et preuve de protocoles adaptatifs pour robots oublieux – SAPPORO
Safe, Adaptive, and Provable Protocols for Oblivious Robots Operation
Les réseaux de robots mobiles peuvent exécuter en coopération des tâches complexes variées. Ils sont caractérisés par la grande variabilité et l’extrême dynamisme de leur structure et de leur environnement d’exécution. Obtenir des garanties fortes sur leur comportement est un enjeu majeur : de nombreuses applications ont un aspect critique et dans un tel contexte distribué un raisonnement informel est susceptible de mener à des erreurs subtiles mais désastreuses une fois le système déployé.
SAPPORO vise à offrir les moyens de vérifier formellement la correction de protocoles distribués et de résultats théoriques dans le cadre des essaims de robots autonomes.
«L’ambition de SAPPORO est de poser des bases formelles et des méthodologies destinés aux développeurs pour essaims de robots mobiles, de permettre la certification de protocoles distribués candidats à l’accomplissement d’une tâche ou bien de montrer formellement l’impossibilité de réaliser un tel protocole. Afin de fournir ces garanties fortes sur les protocoles pour robots mobiles, nous voulons proposer un cadre de développement s’appuyant sur un modèle formel pouvant aider tant spécialistes que non spécialistes de la preuve à établir leur résultats et certifier leurs développements pour essaims de robots. Concevoir ce cadre implique de définir le modèle formel le mieux adapté à ce contexte particulier, de fournir des bibliothèques et techniques de preuve, enfin de fournir un environnement intégré pour à la fois développer et prouver les protocoles distribués. Les trois grands défis de SAPPORO sont donc :<br />1 Que peut-on exprimer formellement ?<br />2 Quelle est la meilleure façon de le faire ?<br />3 Comment peut-on le mettre en pratique ?<br />Le modèle formel est au cœur du projet : toutes les propriétés fondamentales, algorithmes, preuves et outils développés s’appuient sur lui. Il doit permettre d’exprimer les hypothèses typiquement posées par les concepteurs de protocoles, notamment en ce qui concerne l’espace où les robots évoluent, l’environnement et les différents schémas d’exécution, enfin les paradigmes utilisés dans les protocoles.<br />La confiance à accorder aux robots autonomes constitue un enjeu sociétal majeur ; les grands média considèrent la robotique en essaim comme une des « cinq technologies clefs » qui vont tout changer. Parce qu’il est destiné à aider à la fois dans le travail de preuve et dans l’effort de spécification des comportements, SAPPORO assistera la recherche ainsi que l’industrie dans cette tâche indispensable qu’est la fourniture de systèmes distribués sûrs.<br />Le cadre formel sera en particulier librement disponible pour la communauté scientifique.
«L'approche suivie par SAPPORO est de composer et étendre les moyens actuels pour spécifier, concevoir et prouver au sein un environnement facile à appréhender. D'une part il doit permettre de spécifier tant les protocoles distribués que leurs propriétés de façon relativement aisée et ce y compris pour un non spécialiste de la preuve formelle. D'autre part, il doit faciliter le développement de preuves formelles en fournissant bibliothèques de lemmes et techniques d'automatisation. Le modèle est développé en et pour Coq, où ses propriétés sont établies : tous les outils dérivés s'appuiront donc sur une base certifiée solide et cohérente.
Un premier pilier est la formalisation des fondamentaux de la robotique en essaim, permettant de travailler sur des protocoles extrêmement dynamiques et capable de capturer les grandes caractéristiques des scénarios d'application envisagés, à savoir : les espaces multidimensionnels, les exécutions asynchrones et les comportements probabilistes.
Un deuxièmes pilier est la réutilisabilité des notions et étapes de preuves fondamentales afin de faciliter tant les spécifications que les développements de preuves. Cela passe par le développement de bibliothèques et un soin particulier porté à l'automatisation.
À terme il s'agit d'obtenir un environnement intégré de développement et de vérification pour les essaims de robots, articulant un langage de spécification, son générateur de conditions de vérification et le cadre formel, le tout permettant un développement sûr.
à venir
à venir
«- Stand Up Indulgent Rendez-vous. Quentin Bramas, Anissa Lamani, Sébastien Tixeuil. In Proceedings of SSS 2020, Austin, Texas, November 2020.
- Partial Gathering of Mobile Robots from Multiplicity-Allowed Configurations in Rings. Masahiro Shibata, Sébastien Tixeuil. In Proceedings of SSS 2020, Austin, Texas, November 2020.
- Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space. Xavier Défago, Adam Heriban, Sébastien Tixeuil, Koichi Wada. In Proceedings of IEEE SRDS 2020, Shanghai, China, October 2020.
- Du discrètement continu au continûment discret. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain. In Algotel 2020, Lyon, France, October 2020.
- On the Encoding and Solving of Partial Information Games. Yackolley Amoussou-Guenou, Souheib Baarir, Maria Potop-Butucaru, Nathalie Sznajder, Léo Tible and Sébastien Tixeuil. In Proceedings of NETYS 2020, Marrackech, Morocco, June 2020.«
Un modèle émergent est récemment devenu très populaire : les essaims de robots mobiles. Ces robots autonomes peuvent réaliser en collaboration différentes tâches complexes, par exemple l'exploration de zones dévastées pour planifier et aider aux opérations de recherche et secours. Une extrême dynamicité caractérise ce modèle, tant pour la structure, la charge, les données que pour l'environnement d'exécution. Les possibles fautes byzantines, bien connues pour être remarquablement difficiles à appréhender lors de raisonnements informels (et donc sources d'erreurs aux conséquences potentiellement désastreuses une fois le système déployé), rendent cruciale l'obtention de garanties fortes sur le comportement des agents et la correction des protocoles distribués. SAPPORO propose un cadre pour la preuve formelle (mécanisée pour l'assistant à la preuve Coq) destiné au développement sûr des protocoles distribués en interaction locale qui sont au coeur des réseaux dynamiques de capteurs mobiles.
Coordination du projet
Xavier Urbain (UMR 5205 - LABORATOIRE D'INFORMATIQUE EN IMAGE ET SYSTEMES D'INFORMATION)
L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.
Partenaire
LIP6 Laboratoire d'informatique de Paris 6
Tokyo Institute of Technology / DDS
CEDRIC CENTRE D'ETUDES ET DE RECHERCHE EN INFORMATIQUE ET COMMUNICATIONS
LIRIS UMR 5205 - LABORATOIRE D'INFORMATIQUE EN IMAGE ET SYSTEMES D'INFORMATION
Aide de l'ANR 358 959 euros
Début et durée du projet scientifique :
décembre 2019
- 48 Mois
