Ogma: Helper tool to interoperate between Copilot and other languages.
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.
Some use cases supported by Ogma include:
Translating requirements defined in NASA requirements elicitation tool FRET into corresponding monitors in Copilot.
Generating the glue code necessary to work with C structs in Copilot.
Generating NASA Core Flight System applications that use Copilot for monitoring data received from the message bus.
Generating message handlers for NASA Core Flight System applications to make external data in structs available to a Copilot monitor.
Generating Robot Operating System (ROS 2) applications that use Copilot for monitoring data received from different topics.
Generating F' components that use Copilot for monitoring.
The main invocation with --help
lists sub-commands available.
$ ogma --help
ogma - an anything-to-Copilot application generator
Usage: ogma COMMAND
Generate complete or partial Copilot applications from multiple languages
Available options:
-h,--help Show this help text
Available commands:
structs Generate Copilot structs from C structs
handlers Generate message handlers from C structs
cfs Generate a complete CFS/Copilot application
fprime Generate a complete F' monitoring component
fret-component-spec Generate a Copilot file from a FRET Component
Specification
fret-reqs-db Generate a Copilot file from a FRET Requirements
Database
ros Generate a ROS 2 monitoring application
For further information, see:
"Copilot 3", Perez, Dedden and Goodloe. 2020.
"From Requirements to Autonomous Flight", Dutle et al. 2020.