OGMA

Ogma is a tool to facilitate the integration of safe runtime monitors into other systems. Ogma extends Copilot, a high-level runtime verification framework that generates hard real-time C99 code.

Features

• Generating NASA Core Flight System runtime monitoring applications that monitor data received from the message bus.

• Generating Robot Operating System runtime monitoring applications.

• Generating F' (FPrime) runtime monitoring components.

• Generating message handlers for NASA Core Flight System applications to make external data in structs available to a Copilot monitor.

• Generating monitors from diagrams in diagrammatic formats (e.g., DOT/Graphviz, mermaid).

• Generating the glue code necessary to work with C structs in Copilot.

<p align="center"> <img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/simulator.gif" alt="Monitoring within simulation video"> <br /> <i>Integration of monitors into larger applications (e.g., simulators).</i> </p> <p align="center"> <img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/ros.gif" alt="Monitoring within ROS simulation video"> <br /> <i>Integration of monitors into robotics applications.</i> </p>

Table of Contents

• Installation
  • Linux installation
  • Mac installation
  • Troubleshooting
• Usage
  • cFS Application Generation
  • ROS Application Generation
  • F' Component Generation
  • Generating Monitors from Diagrams
  • Struct Interface Generation
• Contributions
• Acknowledgements
• License

Installation

^{(Back to top)}

Linux Installation

^{(Back to top)}

Ubuntu 25.10 / Debian Forky or newer

On Ubuntu 25.10 / Debian Forky or newer, Ogma can be installed directly from the package repositories with:

$ sudo apt-get install ogma

To test that Ogma is available, execute the following to print the list of commands supported:

$ ogma --help

Other Linux distributions

On other Linux distributions or older Debian-based distributions, to use Ogma you must compile it from source, for which you need a number of pre-requisites, such as a Haskell compiler (GHC) and the package manager Cabal (cabal-install), the libraries bz2 and expat, and the theorem prover z3. At this time, we recommend GHC 8.6 and a version of cabal-install between 2.4 and 3.2. (Ogma has been tested with GHC versions up to 9.2 and cabal-install versions up to 3.6, although the installation steps may vary slightly depending on the version of cabal-install being used.)

On Debian or Ubuntu Linux, these dependencies can be installed with:

$ apt-get install ghc cabal-install libz-dev libbz2-dev libexpat-dev z3

Once the compiler is installed, install Ogma from Hackage with:

$ cabal update
$ cabal install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter
$ cabal install ogma-cli:ogma

After that, the ogma executable will be placed in the directory $HOME/.local/bin/, where $HOME represents your user's home directory.

To test that Ogma is available, execute the following to print the list of commands supported:

$ ogma --help

Alternatively, you may want to install the latest development version of Ogma from the official repository, which you can do as follows:

$ git clone https://github.com/nasa/ogma.git
$ cd ogma
$ export PATH="$HOME/.local/bin/:$PATH"
$ cabal update
$ cabal install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter
$ cabal install ogma-cli:ogma

Like before, the ogma executable will be placed in the directory $HOME/.local/bin/, where $HOME represents your user's home directory.

Mac installation

^{(Back to top)}

On macOS, to use Ogma you must compile it from source, for which you need a number of pre-requisites, such as a Haskell compiler (GHC) and the package manager Cabal (cabal-install), as well as the libraries bz2 and expat, and the theorem prover z3.

$ brew install ghc cabal-install bzip2 expat z3

Once the compiler is installed, install Ogma from Hackage with:

$ cabal update
$ cabal install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter
$ cabal install ogma-cli:ogma

After that, the ogma executable will be placed in the directory $HOME/.local/bin/, where $HOME represents your user's home directory.

To test that Ogma is available, execute the following to print the list of commands supported:

$ ogma --help

Alternatively, you may want to install the latest development version of Ogma from the official repository, which you can do as follows:

$ git clone https://github.com/nasa/ogma.git
$ cd ogma
$ export PATH="$HOME/.local/bin/:$PATH"
$ cabal update
$ cabal install --lib copilot copilot-core copilot-c99 copilot-language \
    copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter
$ cabal install ogma-cli:ogma

Like before, the ogma executable will be placed in the directory $HOME/.local/bin/, where $HOME represents your user's home directory.

Troubleshooting

^{(Back to top)}

Feel free to open an issue if you are unable to install Ogma following these instructions.

There is a .github/ directory at the root of the repository that may help with troubleshooting the installation. Also, our issues often include comments with Dockerfiles listing the steps necessary to install Ogma from scratch.

Usage

^{(Back to top)}

The main invocation of ogma with --help lists sub-commands available. More details are provided in the following sections.

cFS Application Generation

NASA Core Flight System (cFS) is a flight software architecture to implement complex systems by combining multiple reusable applications that communicate to one another via a software bus. cFS has been used, among others, on spacecraft, cubesats, and drones.

Ogma includes multiple facilities to generate cFS applications. The cFS applications generated by Ogma perform three steps to connect Copilot monitors to the application:

• Subscribe to a message in the cFS communication bus.
• When a message of the desired kind arrives, copy the data to make it available to Copilot and call the monitor's main entry point.
• Declare handlers that are executed when the property being monitored is violated.

When using this facility, Ogma produces a Copilot file that the user is expected to modify to implement the property to monitor. To avoid having to modify the generated C files that implement the cFS app itself, Ogma gives the ability to state what information one is interested in monitoring. If the kind of information is known to Ogma, it will automatically subscribe to the necessary messages and make it available to Copilot. Ogma provides additional flags to customize the list of known variables, so that projects can maintain their own variable databases beyond what Ogma includes by default.

cFS applications are generated using the Ogma command cfs, which accepts the following arguments:

• --input-file FILENAME: location of the specification or source file for which a cFS application is being generated.
• --target-dir DIR: location where the cFS application files must be stored.
• --template-dir DIR: location of the cFS application template to use.
• --variable-file FILENAME: a file containing a list of variables to monitor in the cFS application.
• --variable-db FILENAME: a file containing a database of known variables, and the message they are included with.
• --handlers-file FILENAME: a file containing a list of known fault handlers or triggers.
• --input-format FORMAT_NAME: the name of a know input format description file in JSON or XML. It can be a path to a file containing such description.
• --prop-format FORMAT_NAME: the name of the format or language in which the properties are encoded. For example, a file may contain a list of properties, and each property may contain a field with a formula in SMV (smv) or Copilot (literal).
• --parse-prop-via COMMAND: a command in the PATH capable of translating properties as listed in the specification file into properties in the target property language. This external process may be a translation tool, or an LLM capable of translating into the target language.
• --template-vars FILENAME: a JSON file containing a list of additional variables to expand in the template.

[!NOTE] Ogma does not guarantee that the result of a translation carried out by calling an external command or LLM with the flag --parse-prop-via is correct. It is your responsibility as the user to check the output produced by the auxiliary translation command for accuracy. Ogma will accept whatever output the command produces as a replacement for the property's formula, and use it without changes if the property format selected is literal, or try to translate it into Copilot if a different property format has been selected. This limitation applies even in the case where the subsequent translation