NASA Ogma

Générateur de moniteurs d'exécution de la NASA pour des systèmes robotiques et de vol sûrs

Licence

Apache-2.0

Aperçu

Ogma est un outil développé par la NASA pour générer des applications de surveillance à l'exécution destinées aux systèmes robotiques et de vol. Il traduit des exigences de sécurité de haut niveau écrites en logique temporelle (par exemple « l'altitude ne doit jamais dépasser X tant que Y est actif ») en code de surveillance C, C++ ou ROS efficace, qui s'exécute aux côtés du système réel. Ogma prend en charge Robot Operating System (ROS/ROS2), les frameworks logiciels de vol cFS/fPrime de la NASA et Space ROS. Il sert à garantir la sûreté de systèmes autonomes lorsque la vérification formelle du système complet n'est pas réalisable en pratique.

NASA Ogma est un outil qui génère des moniteurs d'exécution pour les systèmes robotiques et les logiciels de vol. Il étend Copilot, un framework de vérification à l'exécution de haut niveau, afin de produire du code de surveillance C99 temps réel strict à partir de spécifications en logique temporelle. Les moniteurs générés peuvent être intégrés directement dans des applications ROS, ROS 2, NASA Core Flight System (cFS), F' (fPrime) et Space ROS.

L'outil traduit des spécifications formelles – écrites sous forme d'expressions de logique temporelle, voire de diagrammes visuels aux formats DOT/Graphviz et Mermaid – en applications de surveillance qui observent le comportement du système à l'exécution. Lorsqu'une spécification est violée, le moniteur déclenche des alertes, ce qui permet de détecter tôt les problèmes critiques pour la sûreté avant qu'ils ne dégénèrent en défaillances en cascade.

Ogma est activement maintenu par la NASA, avec plus de 350 commits par an. Il est disponible sous forme de paquet Debian/Ubuntu et via le dépôt Hackage de Haskell. Le projet constitue un pont rare entre la recherche en méthodes formelles et le déploiement concret de la robotique, et rend la vérification à l'exécution de niveau aérospatial accessible à la communauté de la robotique open source.

Pourquoi c'est important

Ogma met la vérification à l'exécution de niveau NASA à la portée de l'ensemble de la communauté robotique. En générant automatiquement des moniteurs à partir de spécifications formelles, il permet aux développeurs d'ajouter des couches de garantie de sûreté aux systèmes ROS, ROS 2 et aux logiciels de vol sans écrire à la main un code de surveillance complexe.

Le problème résolu

Les systèmes robotiques et de vol critiques pour la sûreté nécessitent une surveillance continue à l'exécution pour détecter les violations de spécification, mais écrire à la main un code de surveillance correct est source d'erreurs et prend du temps. Ogma résout ce problème en générant automatiquement des moniteurs C99 temps réel strict à partir de spécifications de haut niveau en logique temporelle, garantissant la correction par construction.

Points clés

• Génère des moniteurs d'exécution à partir de spécifications en logique temporelle, sans code C écrit à la main
• Prend en charge les frameworks ROS, ROS 2, NASA cFS, F' (fPrime) et Space ROS
• Repose sur Copilot, un framework de vérification à l'exécution de haut niveau qui produit du C99 temps réel strict
• Peut générer des moniteurs à partir de diagrammes visuels (DOT/Graphviz, Mermaid)
• Développé et maintenu par la NASA, avec un développement extrêmement actif (plus de 350 commits par an)

Pour qui

• Ingénieurs en robotique qui conçoivent des systèmes critiques pour la sûreté nécessitant une surveillance à l'exécution
• Développeurs de la NASA et de l'aérospatial travaillant avec cFS, fPrime ou Space ROS
• Développeurs ROS/ROS 2 qui ajoutent des couches de vérification formelle à leurs applications
• Chercheurs en systèmes autonomes qui étudient la vérification à l'exécution et la garantie de sûreté

Limites

• Écrit en Haskell, un langage peu familier pour la plupart des développeurs en robotique
• Nécessite de comprendre la logique temporelle pour écrire des spécifications pertinentes
• La génération de moniteurs cible des frameworks spécifiques : les intégrations personnalisées demandent un travail supplémentaire
• Axé sur la surveillance de propriétés, et non sur la vérification formelle complète du comportement du système