[ANN] NASA's Ogma 1.0.9

Hi everyone!

I’m really excited to announce the release of Ogma 1.0.9!

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

Use cases supported by Ogma include producing Robot Operating System (ROS 2) packages [3], NASA Core Flight System (cFS) applications [4], and components for FPrime [1] (the software framework used for the Mars Helicopter), as well as generating monitors from requirements specified in natural language [5]. Ogma is also one of the solutions recommended for monitoring in Space ROS applications [2].

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:

What’s changed

This release improves the user experience and fixes a number of bugs in the code and documentation. A new flag --target-file-name allows users to specify the root for C monitoring files generated by some of the backends, which makes for a simpler process.

For details about the release, see: Release v1.0.9 · 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 Jul 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.

  • Simplify the architecture. More specifically, we now have improved the compilation process by using a higher-kinded data structure, allowing us to incorporate different kinds of information to syntax trees used during both parsing and code generation. This feature has been prototyped, and is currently undergoing testing.

We hope that 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

3 Likes