NASA Ogma

Generador de monitores en tiempo de ejecución de la NASA para sistemas robóticos y de vuelo seguros

Licencia

Apache-2.0

Resumen

Ogma es una herramienta desarrollada por la NASA para generar aplicaciones de monitorización en tiempo de ejecución para sistemas robóticos y de vuelo. Traduce requisitos de seguridad de alto nivel escritos en lógica temporal (por ejemplo, «la altitud nunca debe superar X mientras Y esté activo») en código de monitorización eficiente en C, C++ o ROS que se ejecuta junto al sistema real. Ogma es compatible con Robot Operating System (ROS/ROS2), los marcos de software de vuelo cFS/fPrime de la NASA y Space ROS. Se utiliza para garantizar la seguridad de sistemas autónomos en los que la verificación formal del sistema completo no resulta práctica.

NASA Ogma es una herramienta que genera monitores en tiempo de ejecución para sistemas robóticos y de software de vuelo. Amplía Copilot, un marco de verificación en tiempo de ejecución de alto nivel, para producir código de monitorización C99 de tiempo real estricto a partir de especificaciones de lógica temporal. Los monitores generados pueden integrarse directamente en aplicaciones de ROS, ROS 2, NASA Core Flight System (cFS), F' (fPrime) y Space ROS.

La herramienta traduce especificaciones formales —escritas como expresiones de lógica temporal o incluso como diagramas visuales en formato DOT/Graphviz y Mermaid— en aplicaciones de monitorización que observan el comportamiento del sistema en tiempo de ejecución. Cuando se incumple una especificación, el monitor activa alertas, lo que permite detectar a tiempo problemas críticos para la seguridad antes de que deriven en fallos en cadena.

La NASA mantiene Ogma activamente, con más de 350 commits al año. Está disponible como paquete de Debian/Ubuntu y a través del repositorio Hackage de Haskell. El proyecto constituye un puente poco común entre la investigación en métodos formales y el despliegue práctico de la robótica, y pone la verificación en tiempo de ejecución de nivel aeroespacial al alcance de la comunidad de robótica de código abierto.

Por qué importa

Ogma lleva la verificación en tiempo de ejecución de nivel NASA a la comunidad de robótica en general. Al generar automáticamente monitores a partir de especificaciones formales, permite a los desarrolladores añadir capas de garantía de seguridad a sistemas ROS, ROS 2 y de software de vuelo sin escribir a mano código de monitorización complejo.

Qué problema resuelve

Los sistemas robóticos y de vuelo críticos para la seguridad necesitan una monitorización continua en tiempo de ejecución para detectar incumplimientos de la especificación, pero escribir a mano un código de monitorización correcto es propenso a errores y requiere mucho tiempo. Ogma lo resuelve generando automáticamente monitores C99 de tiempo real estricto a partir de especificaciones de lógica temporal de alto nivel, lo que garantiza la corrección por construcción.

Puntos clave

• Genera monitores en tiempo de ejecución a partir de especificaciones de lógica temporal, sin necesidad de escribir código C a mano
• Compatible con los marcos ROS, ROS 2, NASA cFS, F' (fPrime) y Space ROS
• Basado en Copilot, un marco de verificación en tiempo de ejecución de alto nivel que produce C99 de tiempo real estricto
• Puede generar monitores a partir de diagramas visuales (DOT/Graphviz, Mermaid)
• Desarrollado y mantenido por la NASA, con un desarrollo muy activo (más de 350 commits al año)

Para quién es

• Ingenieros de robótica que construyen sistemas críticos para la seguridad que requieren monitorización en tiempo de ejecución
• Desarrolladores de la NASA y del sector aeroespacial que trabajan con cFS, fPrime o Space ROS
• Desarrolladores de ROS/ROS 2 que añaden capas de verificación formal a sus aplicaciones
• Investigadores de sistemas autónomos que estudian la verificación en tiempo de ejecución y la garantía de seguridad

Limitaciones

• Escrito en Haskell, un lenguaje que puede resultar desconocido para la mayoría de los desarrolladores de robótica
• Requiere comprender la lógica temporal para escribir especificaciones significativas
• La generación de monitores se dirige a marcos específicos; las integraciones personalizadas requieren trabajo adicional
• Centrado en la monitorización de propiedades, no en la verificación formal completa del comportamiento del sistema