[Master] Sûreté des essaims de robots mobiles

Couverture de zone et vision contrainte

Encadrant : Lionel Rieg

Les réseaux de robots autonomes permettent d’utiliser des comportements émergeant de protocoles distribués simples, tout en garantissant une grande résilience et flexibilité dans la taille de l’essaim. Lorsqu’un essaim de robots mobiles est utilisés dans un cadre critique, par exemple lorsque des vies sont en jeu, il est impératif d’avoir les plus fortes garanties de correction possibles sur les protocoles, c’est-à-dire sur le comportement de l’essaim par rapport à ce qu’on en attend. On s’intéresse donc à la preuve formelle dans le cadre des robots mobiles, en particulier avec l’assistant de preuve Coq et la bibliothèque Pactole.

Le but de ce travail est de proposer un mécanisme de dispersion, sans collision, de robots à vision limitée afin d’obtenir une couverture d’une zone prédéfinie, dans un cadre de perception imparfaite (par masquage ou imprécisions des capteurs). On s’attachera à modéliser voire prouver formellement la correction du nouveau protocole obtenu.

Pour plus de détails, voir la description pdf.


Documents joints

Stage M2 robots couverture

20 décembre 2022
info document : PDF
77.8 kio

Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4193712