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. |
The development of autonomous robotic systems uses intelligent functions, system control, data treatment or trajectory planning. These functions are implemented through programmation environments such as ROS, which results in complex software architectures, where dozens of processus run together.
The design of autonomous missions demands high-level behavior specifications, which lie on functions given by the robotic system. These behaviors require to be robust if problems arise (for instance, sensor failure), or external events due to the mission and its environment. Furthermore, in critical contexts, high risk missions or when the intervention of a human operator is impossible, it is necessary to bring proofs on the robust and correct behavior of the system. To that end, classical test methods or simulations can prove insufficient for the system.
This thesis subject aims to tackle the problematic of specification and analysis of behaviors, through formal methods. Formal methods and Petri networks in particular will be studied for its convenience when specifying concurrent behaviors, possibility to run models, as well as existing tools for model-checking. |