Résumé
Le développement de systèmes robotiques autonomes met en oeuvre des fonctionnalités intelligentes, de contrôle du système, de traitement de ses données, ou de planification de sa trajectoire. Ces fonctionnalités sont implantées au travers d’environnements de programmation tels que ROS, ce qui résulte en des architectures logicielles complexes, faisant intervenir plusieurs dizaines de processus.La réalisation de missions en autonomie nécessite de pouvoir spécifier des comportements haut-niveau, qui reposent sur les fonctionnalités fournies par le système robotique. Ces comportements nécessitent d’être robustes à la survenue de pannes sur le système robotique (par ex. pannes de capteurs), ou à des événements extérieurs liés à la mission et à son environnement. De plus, dans des contextes critiques, pour des missions risquées ou lorsque l’intervention d’un opérateur humain est quasiment impossible, il est nécessaire d’apporter des preuves a priori sur le comportement robuste et correct du système. Dans ce cadre, les techniques classiques de tests ou de simulation peuvent se révéler insuffisants à garantir une confiance suffisante dans le système.Ce sujet de thèse vise à aborder cette problématique de la spécification et de l’analyse de comportements, au moyen de méthodes formelles. Le formalisme des réseaux de Petri sera en particulier étudié de par son adéquation à la spécification de comportements concurrents, la possibilité d’exécuter les modèles, ainsi que les outils de model-checking existants.