Le thème Architecture Décisionnelle recouvre des recherche dans les domaines suivants:

Validation et Vérification en Robotique

Intégration de la Décision en Robotique

Validation et Vérification en Robotique

L'objectif à long terme de cette recherche est d'offrir la possibilité de valider et de vérifier l'ensemble des logiciels qui composent un système autonome, du niveau le plus bas des boucles de contrôle jusqu'aux fonctions délibératives.

Ce travail bénéficie grandement de notre collaboration avec l'équipe VERTICS dont les outils et les approches (Fiacre, TINA, Hippo) sont bien adaptés aux problèmes que nous voulons traiter.

L'approche que nous poursuivons se caractérise de la façon suivante :

• L'approche actuelle englobe les composants fonctionnels et les compétences (skills) d'action.
• Ces composants fonctionnels sont entièrement spécifiés avec GenoM par les programmeurs de robots (non experts en modèles formels) et l'implémentation régulière des composants est déjà automatiquement synthétisée à partir de ces spécifications.
• Les skills sont spécifiées avec un nouveau langage ProSkill qui combine le langage de skills décrit dans [Albore et al., 2023, Fig. 7] (pour les skills de base, c'est-à-dire celles qui font appel aux services des composants) et le langage procédural déployé dans OpenPRS [Ingrand et al., 1996] (pour les skills composites combinant les skills de base et les skills composites).
• Les modèles formels en Fiacre sont automatiquement synthétisés à partir de ces spécifications (à la fois pour les composants et les skills) et, pour le composant, ils ont une sémantique cohérente avec celle de l'implémentation régulière du composant.
• Les modèles formels synthétisés dans Fiacre peuvent ensuite être utilisés à la fois hors ligne (avec Tina) pour la vérification avec des outils de model-checking et en ligne (avec Hippo) pour la vérification de l'exécution et la vérification de propriété à la volée.

Les résultats les plus récents sont les suivants :

• Un modèle Fiacre/H-Fiacre complet et fiable de tout composant du GenoM. Le modèle est si proche de l'implémentation du composant normal que nous ne pouvons pas les distinguer lorsqu'ils s'exécutent sur nos robots.
• Un moteur Hippo capable d'exécuter complètement n'importe quel modèle H-Fiacre de composants GenoM,
• Des expériences complexes où le moteur Hippo exécute le modèle complet et tourne à bord d'un ordinateur embarqué de drone et le contrôle à 10 kHz.
• Proskill, un nouveau langage de skills (compétences) qui nous permet de contrôler de multiples composants avec des programmes complexes (incluant test, parallélisme, boucle) tout en prenant en compte les préconditions, les effets, les invariants sur les skills et en modélisant les événements externes ainsi que les transitions des variables d'état.

De nombreux défis restent à relever :

• la V&V des modèles appris, qu'ils soient utilisés pour la perception ou la prise de décision, dont la sensibilité à des changements mineurs dans les données d'entrée entraîne des faux positifs qui interdisent leur utilisation dans des systèmes critiques.
• l'intégration, la cohérence et l'interopérabilité des différents modèles formels utilisés dans les différentes composantes du système.
• l'intégration des êtres humains dans les modèles et dans le processus de vérification, qu'ils soient membres de l'équipe, assistants, utilisateurs ou simplement présents dans l'environnement, etc.
• le déploiement systématique de moniteurs de sécurité basés sur des modèles formels opérationnels, qui resteraient l'ultime garde-fou lorsque les méthodes hors ligne ont montré leurs limites.

Publications:

• A formal toolchain for offline and run-time verification of robotic systems Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩
• Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin Journal of Systems and Software, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩

Intégration de la Décision en Robotique