ANN: NASA's Ogma 1.0.8 -- now with FPrime support

Hi everyone!

I’m thrilled to announce the release of Ogma 1.0.8!

Ogma is a NASA tool that facilitates integrating runtime monitors or runtime verification applications into other systems.

This is one of the biggest releases of Ogma ever: We can now generate monitors for FPrime [1], a component-based flight software framework used in many missions, including NASA’s Ingenuity Mars Helicopter.

The Ingenuity Mars Helicopter is a technology demonstration to test powered, controlled flight on another world for the first time. It hitched a ride to Mars on the Perseverance rover. The Mars Helicopter has, since its launch, completed 47 flights (and counting!). Credits: NASA/JPL-Caltech. Disclaimer: Ogma-generated monitors are NOT currently running as part of the Ingenuity mission.

Since the last release, Ogma also has officially become one of the solutions recommended for monitoring in Space ROS applications [2].

Use cases supported by Ogma also include producing Robot Operating System (ROS 2) packages [3] and NASA Core Flight System (cFS) monitoring applications [4], and generating monitors directly from requirements specified using a structure natural language framework [5]. Ogma leverages existing Haskell work, like the Copilot language [6] (also funded by NASA) and BNFC [7].

For more details, including videos of monitors being generated and flown in simulators, see:

Changelog

The changelog is available at: Release v1.0.8 · nasa/ogma · GitHub

Releases

Ogma is released as a collection of packages in Hackage. The entry point is ogma-cli: Ogma: Helper tool to interoperate between Copilot and other languages..

Code

The github repo is located at: GitHub - nasa/ogma.

What’s coming

The next release is planned for May 21st, 2023.

Ogma is currently undergoing the qualification process necessary for NASA Class D Software. Apart from the changes required by that process, we also have the following in our roadmap:

  • Extend ROS 2 monitors with further information about sources of violations.
  • Add tests to generated code.
  • Simplify NASA cFS monitor generation process.

We hope you are as excited as we are and that our work demonstrates that, with the right support, Haskell can reach farther than we ever thought possible.

Happy Haskelling!

Ivan

[1] GitHub - nasa/fprime: F' - A flight software and embedded systems framework

[2] https://space.ros.org/

[3] https://www.ros.org/

[4] GitHub - nasa/cFS: The Core Flight System (cFS)

[5] GitHub - NASA-SW-VnV/fret: A framework for the elicitation, specification, formalization and understanding of requirements.

[6] GitHub - Copilot-Language/copilot: A stream-based runtime-verification framework for generating hard real-time C code.

[7] GitHub - BNFC/bnfc: BNF Converter

5 Likes