Abstract : The proof of safety of robotic systems is a fundamental issue for the development of robotics. It consists, for instance, in verifying that a robot control law will always satisfy a set of constraints. More generally, we will be interested here in the verification of the properties of dynamical systems that allow to model the evolution of a robot.
The main contribution of this thesis is to provide a new way of bracketing invariant sets of dynamical systems. To this end, a new abstract domain, the mazes, and new algorithms are presented. It is also shown, through many examples, how classic validation problems can be translated into a problem of bracketing invariant sets. Finally, the results are extended to the bracket of viability kernels.
This thesis is also based on an application in underwater robotics. The main idea is to use ocean currents so that an underwater robot can efficiently travel long distances. A new kind of low-cost autonomous robot has been developed for this type of mission. This new hybrid profiling float is able to regulate its depth with a new regulation law, but also to correct its trajectory using auxiliary thrusters. They allow the robot to choose the right flow of current to be used. The previously introduced validation tools are applied to validate the robot and the mission safety. Experiments in real conditions also enabled the prototype to be validated.
Résumé : La vérification de la sûreté de fonctionnement des systèmes robotiques est une question fondamentale pour le développement de la robotique. Elle consiste, par exemple, à vérifier qu’une loi de commande d’un robot respectera toujours un ensemble de contraintes. Plus généralement, nous nous intéresserons ici à la vérification des propriétés de systèmes dynamiques, ces derniers permettant de modéliser l’évolution d’un robot.
La contribution principale de cette thèse est d’apporter un nouveau moyen d’encadrer les ensembles invariants de systèmes dynamiques. Pour cela, un nouveau domaine abstrait, les mazes, et de nouveaux algorithmes sont présentés. Il est également montré, au travers de nombreux exemples, comment des problèmes classiques de validation peuvent être ramenés à un problème d’encadrement d’ensembles invariants. Enfin, les résultats sont étendus à l’encadrement des noyaux de viabilités.
Cette thèse s’appuie également sur une application en robotique sous-marine. L’idée principale est d’utiliser les courants marins pour qu’un robot sous-marin puisse parcourir avec efficience de grandes distances. Un nouveau type de robot autonome bas coûts a été développé pour ce type de mission. Ce nouveau flotteur profileur hybride est capable de se réguler en profondeur grâce à une nouvelle loi de régulation, mais également de corriger sa trajectoire à l’aide de propulseurs auxiliaires. Ils permettent au robot de choisir la bonne veine de courant à emprunter. Les outils de validations précédemment introduits sont utilisés pour valider la sûreté du robot et de la mission. Des expérimentations en conditions réelles ont également permis de valider le prototype.