NASA Ogma

NASA runtime monitor generator for safe robotics and flight systems

License

Apache-2.0

Overview

Ogma is a NASA-developed tool for generating runtime monitoring applications for robotics and flight systems. It translates high-level safety requirements written in temporal logic (e.g., 'the altitude must never exceed X while Y is active') into efficient C, C++, or ROS monitoring code that runs alongside the actual system. Ogma supports Robot Operating System (ROS/ROS2), NASA's cFS/fPrime flight software frameworks, and Space ROS. Used for safety assurance of autonomous systems where formal verification of the full system is impractical.

NASA Ogma is a tool that generates runtime monitors for robotics and flight software systems. It extends Copilot, a high-level runtime verification framework, to produce hard real-time C99 monitoring code from temporal logic specifications. The generated monitors can be integrated directly into ROS, ROS 2, NASA Core Flight System (cFS), F' (fPrime), and Space ROS applications.

The tool works by translating formal specifications — written as temporal logic expressions or even visual diagrams in DOT/Graphviz and Mermaid format — into monitoring applications that observe system behavior at runtime. When a specification is violated, the monitor triggers alerts, enabling early detection of safety-critical issues before they cascade into failures.

Ogma is actively maintained by NASA with over 350 commits per year. It is available as a Debian/Ubuntu package and through Haskell's Hackage repository. The project represents a rare bridge between formal methods research and practical robotics deployment, making aerospace-grade runtime verification accessible to the open-source robotics community.

Why it matters

Ogma brings NASA-grade runtime verification to the broader robotics community. By automatically generating monitors from formal specifications, it enables developers to add safety assurance layers to ROS, ROS 2, and flight software systems without manually writing complex monitoring code.

Problem it solves

Safety-critical robotics and flight systems need continuous runtime monitoring to detect specification violations, but writing correct monitoring code by hand is error-prone and time-consuming. Ogma solves this by auto-generating hard real-time C99 monitors from high-level temporal logic specifications, ensuring correctness by construction.

Key takeaways

• Generates runtime monitors from temporal logic specs — no manual C code needed
• Supports ROS, ROS 2, NASA cFS, F' (fPrime), and Space ROS frameworks
• Built on Copilot, a high-level runtime verification framework producing hard real-time C99
• Can generate monitors from visual diagrams (DOT/Graphviz, Mermaid)
• Developed and maintained by NASA with extremely active development (350+ commits/year)

Who it is for

• Robotics engineers building safety-critical systems that require runtime monitoring
• NASA and aerospace developers working with cFS, fPrime, or Space ROS
• ROS/ROS 2 developers adding formal verification layers to their applications
• Autonomous systems researchers studying runtime verification and safety assurance

Limitations

• Written in Haskell, which may be unfamiliar to most robotics developers
• Requires understanding of temporal logic to write meaningful specifications
• Monitor generation targets specific frameworks — custom integrations need additional work
• Focused on property monitoring, not full formal verification of system behavior