La vérification des robots autonomes, une approche ascendante du roboticien

De nombreuses approches sont envisageables pour la V&V du logiciel d'un RA, comme par exemple rédiger des spécifications de haut niveau et les dériver dans des implémentations correctes, déployer et développer des formalismes de V&V nouvelles ou modifiées pour programmer des composants robotiques, etc. Mis à part les modèles appris, la plupart des modèles utilisés dans les fonctions de délibération [2] se prêtent à la V&V formelle [1] et nous préférons nous concentrer sur le défi de la V&V au niveau fonctionnel. Nous proposons une approche qui s'appuie sur un cadre de spécification / d’implémentation robotique existant (GenoM) pour développer des composants fonctionnels robotiques, auxquels nous associons des cadres formels de V&V existants bien connus (UPPAAL, BIP, FIACRE / TINA).

GenoM a été conçu à l'origine par des roboticiens et des ingénieurs logiciels qui souhaitaient spécifier clairement et précisément comment un composant fonctionnel réutilisable, portable et indépendant du middleware devait être écrit et mis en œuvre. De nombreuses expériences robotiques complexes ont été élaborées et menées sur 20 ans avec GenoM et ce n'est que récemment que ses concepteurs ont réalisé que la spécification rigoureuse, une sémantique claire de la mise en œuvre et le mécanisme de modèle pour synthétiser le code ouvrent la porte à la synthèse automatique de modèles formels et à la V&V formelle (hors ligne et en ligne).

Cette approche ascendante, qui part de la mise en œuvre des composants, peut être plus modeste que les approches descendantes qui visent une vision plus large et plus globale du problème. Pourtant, elle donne des résultats encourageants sur des implémentations réelles sur lesquelles on peut construire des propriétés de haut niveau plus complexes qui devront être ensuite vérifiées et validées hors ligne mais aussi avec des moniteurs en ligne.

Un projet présenté lors du colloque scientifique organisé par Robagri pendant le FIRA 2019:

Références

[1] Félix Ingrand. Recent Trends in Formal Validation and Verification of Autonomous Robots Software [Tendances récentes en matière de validation et de vérification formelles des logiciels de robots autonomes.] Conférence internationale de l'IEEE sur l'informatique robotique, février 2019, Naples, Italie. ⟨Hal-01968265⟩ https://hal.laas.fr/hal-019682

[2] Félix Ingrand, Malik Ghallab. Deliberation for autonomous robots: A survey. Artificial Intelligence [Délibération pour les robots autonomes: Une enquête. Intelligence artificielle], Elsevier, 2017, 247 pp.10-44. ⟨http://www.sciencedirect.com/⟩. ⟨10.1016/j.artint.2014.11.003⟩https://hal.laas.fr/hal-011379

[3] Tesnim Abdellatif, Saddek Bensalem, Jacques Combaz, Lavindra de Silva, Félix Ingrand. Rigorous design of robot software: A formal component-based approach. Robotics and Autonomous Systems [Conception rigoureuse du logiciel du robot: Une approche formelle basée sur les composants. Robotique and Systèmes Autonomes], Elsevier, 2012, 60 (12), pp.1563-1578. ⟨10.1016/j.robot.2012.09.005⟩. https://hal.laas.fr/hal-019800

[4] Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand. On the Semantics of the GenoM3 Framework. [Sur la sémantique du cadre GenoM3]

Rapport LAAS n° 19036. 2019. https://hal.laas.fr/hal-019924