Description
Date depot: 1 janvier 1900
Titre: Approche Formelle pour les Robots Autonomes, Intelligents et Distribués
Directrice de thèse:
Béatrice BÉRARD (LIP6)
Directrice de thèse:
Maria POTOP-BUTUCARU (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Ce sujet de thèse fait suite au projet AFRAID, soutenu par le LIP6, qui initiait une coopération entre les équipes MoVe, NPA et REGAL du laboratoire. Il se situe dans le cadre de la vérification et du contrôle des 'cyber-physical systems'', qui constitue une cible
privilégiée des stratégies de recherche actuelles. L'objectif du travail est la recherche de
stratégies applicables à des protocoles d'exploration pour des réseaux de robots.
{{{1. Problématique}}}
Les tâches susceptibles d'être exécutées par des robots autonomes sont de plus en plus nombreuses et en complexité croissante, que ce soit dans notre environnement quotidien, pour la production industrielle ou même dans l'espace. En particulier, l'époque des robots spécialisés et isolés laisse maintenant la place aux réseaux de robots, par exemple pour l'exploration de zones inaccessibles ou à risque, qui en représente une des applications les plus populaires. Pour remplir leur tâche, ces robots doivent être capables de réaliser des calculs de façon indépendante, de se synchroniser entre eux via la vision ou l'envoi de messages et de se déplacer tout en maintenant la connectivité du réseau qui les relie.
Jusqu'à présent, les réseaux de robots ont été étudiés d'une manière empirique et la plupart des résultats ont été validés principalement par des simulations ou des preuves partielles. Les fonctionnements défectueux de réseaux qui évoluent de manière autonome, à des distances rendant les interventions impossibles, peuvent avoir des conséquences catastrophiques. Ainsi, l'utilisation de méthodes automatiques de vérification et de contrôle est une étape essentielle pour garantir la fiabilité et la robustesse de ces systèmes.
{{{2. Contexte}}}
Les bases de l'étude des protocoles répartis pour les réseaux de robots ont été posées par les travaux de Suzuki et Yamashita, qui définissent le modèle du système et des communications : les robots sont des points dans un plan, qui possèdent une vision globale du système et exécutent un algorithme à trois phases composé d'une prise de vue, un
calcul et un déplacement. Le calcul leur permet de décider leur nouvelle position qui sera mise à jour lors de la phase de mouvement.
Depuis la publication des travaux de Suzuki et Yamashita, plusieurs algorithmes déterministes ou probabilistes ont été proposés pour différents protocoles auto-organisants (dispersion, rassemblement, élection etc.). Cependant, aucun de ces algorithmes n'a été vérifié formellement, leur correction étant prouvée manuellement via des invariants.
Doctorant.e: Millet Laure