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.

Integration of monitors into larger applications (e.g., simulators).

Integration of monitors into robotics applications.

Table of Contents

• Installation
  • Pre-requisites
  • Compilation
• Usage
  • cFS Application Generation
  • ROS Application Generation
  • F’ Component Generation
  • Generating Monitors from Diagrams
  • Struct Interface Generation
• Contributions
• Acknowledgements
• License

Installation

^{(Back to top)}

Pre-requisites

^{(Back to top)}

To install Ogma from source, users must have the tools GHC and cabal-install, as well as the libraries bz2 and expat. 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 libbz2-dev libexpat-dev

On Mac, they can be installed with:

$ brew install ghc cabal-install bzip2 expat

Compilation

^{(Back to top)}

Once GHC and cabal are installed, the simplest way to install Ogma is with:

$ git clone https://github.com/nasa/ogma.git
$ cd ogma
$ export PATH="$HOME/.local/bin/:$PATH"
$ cabal update
$ cabal install --lib copilot copilot-c99 copilot-language copilot-theorem \
    copilot-libraries copilot-interpreter
$ 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.

Usage

^{(Back to top)}

The main invocation of ogma with --help lists sub-commands available. More

File truncated at 100 lines see the full file