Encadrement des plus grands ensembles invariants de systèmes dynamiques : une application aux robots sous-marins dérivant dans les courants océaniques

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.The proof of safety of robotic systems is afundamental issue for the development of robotics. Itconsists, for instance, in verifying that a robot controllaw will always satisfy a set of constraints. More gen-erally, we will be interested here in the verificationof the properties of dynamical systems that allow tomodel the evolution of a robot.The main contribution of this thesis is to providea new way of bracketing invariant sets of dynami-cal systems. To this end, a new abstract domain, themazes, and new algorithms are presented. It is alsoshown, through many examples, how classic valida-tion problems can be translated into a problem ofbracketing invariant sets. Finally, the results are ex-tended to the bracket of viability kernels.This thesis is also based on an application in un-derwater robotics. The main idea is to use oceancurrents so that an underwater robot can efficientlytravel long distances. A new kind of low-cost au-tonomous robot has been developed for this type ofmission. This new hybrid profiling float is able to reg-ulate its depth with a new regulation law, but also tocorrect its trajectory using auxiliary thrusters. Theyallow the robot to choose the right flow of current tobe used. The previously introduced validation toolsare applied to validate the robot and the missionsafety. Experiments in real conditions also enabledthe prototype to be validated