Foughali, Mohammed
[VerfasserIn]
;
Toulouse, INSA
[MitwirkendeR];
Ghallab, Malik
[MitwirkendeR];
Ingrand, Félix
[MitwirkendeR]
Vérification Formelle des Modules Fonctionnels de Systèmes Robotiques et Autonomes ; Formal verification of the functionnal layer of robotic and autonomous systems
Titel:
Vérification Formelle des Modules Fonctionnels de Systèmes Robotiques et Autonomes ; Formal verification of the functionnal layer of robotic and autonomous systems
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 ...