Les systèmes robotiques et autonomes ne cessent d’évoluer et deviennent de plus en plus impliqués dans les missions à coût considérable et/ou dans les milieux humains. Par conséquent, les simulations et campagnes de tests ne sont plus adaptées à la problématique de sûreté et fiabilité des systèmes robotiques et autonomes compte tenu (i) du caractère sérieux des défaillances éventuelles dans les contextes susmentionnés (un dommage à un robot très coûteux ou plus dramatiquement une atteinte aux vies humaines) et (ii) de la nature non exhaustive de ces techniques (les tests et simulations peuvent toujours passer à côté d’un scénario d’exécution catastrophique.Les méthodes formelles, quant à elles, peinent à s’imposer dans le domaine de la robotique autonome, notamment au niveau fonctionnel des robots, i.e. les composants logiciels interagissant directement avec les capteurs et les actionneurs. Elle est due à plusieurs facteurs. D’abord, les composants fonctionnels reflètent un degré de complexité conséquent, ce qui mène souvent à une explosion combinatoire de l’espace d’états atteignables (comme l’exploration se veut exhaustive). En outre, les composants fonctionnels sont décrits à travers des languages et frameworks informels (ROS, GenoM, etc.). Leurs spécifications doivent alors être traduites en des modèles formels avant de pouvoir y appliquer les méthodes formelles associées. Ceci est souvent pénible, lent, exposé à des erreurs, et non automatique, ce qui implique un investissement dans le temps aux limites de la rentabilité. Nous proposons, dans cette thèse, de connecter GenoM3, un framework de développement et déploiement de composants fonctionnels robotiques, à des langages formels et leurs outils de vérification respectifs. Cette connexion se veut automatique: nous développons des templates en mesure de traduire n’importe quelle spécification de GenoM3 en langages formels. Ceci passe par une formalisation de GenoM3: une sémantique formelle opérationnelle est donnée au langage. Une traduction à partir de cette sémantique est réalisée vers des langages formels et prouvée correcte par bisimulation. Nous comparons de différents langages cibles, formalismes et techniques et tirerons les conclusions de cette comparaison. La modélisation se veut aussi, et surtout, efficace. Un modèle correct n’est pas forcément utile. En effet, le passage à l’échelle est particulièrement important.Cette thèse porte donc sur l'applicabilité des méthodes formelles aux compo-sants fonctionnels des systèmes robotiques et autonomes. Le but est d'aller vers des robots autonomes plus sûrs avec un comportement plus connu et prévisible. Cela passe par la mise en place d'un mécanisme de génération automatique de modèles formels à partir de modules fonctionnels de sys-tèmes robotiques et autonomes. Les langages et outils cibles sont Fiacre/TINA et UPPAAL (model checking), UPPAAL-SMC (statistical model checking), BIP/RTD-Finder (SAT solving), et BIP/Engine (enforcement de propriétés en ligne). Les modèles générés sont exploités pour vérifier des propriétés quali-tatives ou temps-réel, souvent critiques pour les systèmes robotiques et auto-nomes considérés. Parmi ces propriétés, on peut citer, à titre d'exemple, l'ordonnançabilité des tâches périodiques, la réactivité des tâches spora-diques, l'absence d’interblocages, la vivacité conditionnée (un évènement tou-jours finit par suivre un autre), la vivacité conditionnée bornée (un évène-ment toujours suit un autre dans un intervalle de temps borné), l'accessibilité (des états “indésirables” ne sont jamais atteints), etc.La thèse propose éga-lement une analyse du feedback expérimental afin de guider les ingénieurs à exploiter ces méthodes et techniques de vérification efficacement sur les mo-dèles automatiquement générés. / The goal of this thesis is to add to the efforts toward the long-sought objective of secure and safe robots with predictable and a priori known behavior. For the reasons given above, formal methods are used to model and verify crucial properties, with a focus on the functional level of robotic systems. The approach relies on automatic generation of formal models targeting several frameworks. For this, we give operational semantics to a robotic framework, then several mathematically proven translations are derived from such semantics. These translations are then automatized so any robotic functional layer specification can be translated automatically and promptly to various frameworks/languages. Thus, we provide a mathematically correct mapping from functional components to verifiable models. The obtained models are used to formulate and verify crucial properties (see examples above) on real-world complex robotic and autonomous systems. This thesis provides also a valuable feedback on the applicability of formal frameworks on real-world, complex systems and experience-based guidelines on the efficient use of formal-model automatic generators. In this context, efficiency relates to, for instance, how to use the different model checking tools optimally depending on the properties to verify, what to do when the models do not scale with model checking (e.g. the advantages and drawbacks of statistical model checking and runtime verification and when to use the former or the latter depending on the type of properties and the order of magnitude of timing constraints).

Dans cette thèse, on s’intéresse à la commande des robots marcheurs. Contrôler ces systèmes naturellement instables, de dynamique non linéaire, non convexe, de grande dimension, et dépendante des contacts représente un défi majeur en robotique mobile. Les approches classiques formulent une chaîne de contrôle formée d’une cascade de sous problèmes tels que la perception, le planning, la commande du corps complet et l’asservissement articulaire. Les contributions rapportées ici ont toutes pour but d’introduire une rétroaction au niveau de la commande du corps complet ou du planning. Précisément, une première contribution technique est la formulation et la comparaison expérimentale de deux estimateurs de la base du robot. Une seconde contribution est l’implémentation d’un contrôleur par dynamique inverse pour contrôler en couple le robot HRP-2. Une variante de ce contrôleur est aussi formulée et testée en simulation pour stabiliser un robot en contact flexible avec son environnement. Finalement un générateur de marche par commande pré-dictive et couplé à un contrôleur corps complet est présenté. / In this thesis, we are interested in the control of walking robots. Controlling these naturally unstable, non-linear, non-convex, large and contact-dependent systems is a major challenge in mobile robotics. Traditional approaches formulate a chain of control formed by a cascade of sub-problems such as perception, planning, full body control and joint servoing. The contributions reported here are all intended to provide state feedback at the whole body control stage or at the planning stage. Specifically, a first technical contribution is the formulation and experimental comparison of two estimators of the robot base. A second contribution is the implementation of a reverse dynamic controller to control the HRP-2 robot in torque. A variant of this controller is also formulated and tested in simulation to stabilize a robot in flexible contact with its environment. Finally, a predictive control operation generator coupled to a whole body controller is presented.