Skip to content

Commit

Permalink
ogma-cli: Structure README around backends. Refs #75.
Browse files Browse the repository at this point in the history 
The README is too focused on the frontends, but most users will mostly
care about the backends.

This commit re-structures the README around the targets or backends,
which are the ones what most users will care the most about.
  • Loading branch information
@ivanperez-keera
ivanperez-keera committed Jan 18, 2024
1 parent 6f0f1f4 commit 5d07b72
Showing 1 changed file with 17 additions and 275 deletions.
292 changes: 17 additions & 275 deletions ogma-cli/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,31 +7,20 @@ verification framework that generates hard real-time C99 code.

# Features

- Translating requirements defined in [NASA's requirements elicitation tool
FRET](https://github.com/NASA-SW-VnV/fret) into corresponding monitors in
Copilot.
- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) runtime
monitoring applications that monitor data received from the message bus.

- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) applications
that use Copilot for monitoring data received from the message bus.
- Generating [Robot Operating System](https://ros.org) runtime monitoring
applications.

- Generating [F' (FPrime)](https://github.com/nasa/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 the glue code necessary to work with C structs in Copilot.

- Generating [Robot Operating System](https://ros.org) applications that use
Copilot for monitoring data published in different topics.

- Generating [F' (FPrime)](https://github.com/nasa/fprime/) components that use
Copilot for monitoring data published in different ports.


<p align="center">
<img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/fret-to-c.gif" alt="Conversion of requirements into C code">
<br />
<i>Conversion of FRET requirements into C code.</i>
</p>

<p align="center">
<img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/simulator.gif" alt="Monitoring within simulation video">
<br />
Expand All @@ -44,7 +33,6 @@ verification framework that generates hard real-time C99 code.
- [Pre-requisites](#pre-requisites)
- [Compilation](#compilation)
- [Usage](#usage)
- [Language Transformations: FRET](#language-transformations-fret)
- [cFS Application Generation](#cfs-application-generation)
- [ROS Application Generation](#ros-application-generation)
- [F' Component Generation](#f-component-generation)
Expand Down Expand Up @@ -98,215 +86,8 @@ After that, the `ogma` executable will be placed in the directory
# Usage
<sup>[(Back to top)](#table-of-contents)</sup>

The main invocation of `ogma` with `--help` lists sub-commands available:
```sh
$ 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 package
```
## Language transformations: FRET
<sup>[(Back to top)](#table-of-contents)</sup>
[FRET](https://github.com/NASA-SW-VnV/fret) is a requirements elicitation tool
created by NASA Ames Research Center. Requirements can be specified in
structured natural language called FRETish, and the tool helps users understand
them, validate them, and formalize them. For instructions on how to specify,
analyze and export FRET requirements, see [the FRET
manual](https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/userManual.md).
<p align="center">
<img src="https://raw.githubusercontent.com/nasa/ogma/develop/docs/fret.png" width="75%">
<br />
<sup><i>Screenshot of requirement specified inside NASA's requirements elicitation tool FRET.</i></sup>
</p>

Ogma can convert specifications generated by FRET into Copilot monitors.
Specifically, the commands `fret-component-spec` and `fret-reqs-db` allow users
to interact with the different kinds of files produced by FRET.

FRET files include properties encoded using Temporal Logic, both in
[SMV](http://www.cs.cmu.edu/~modelcheck/smv.html) and in
[CoCoSpec](https://link.springer.com/chapter/10.1007%2F978-3-319-41591-8_24),
the latter of which is an extension of Lustre. Ogma uses the SMV expressions by
default, but the CLI flag `--cocospec` can be used to select the CoCoSpec
variant of requirements instead.

As an example, from the following FRET requirement:
```
test_component shall satisfy (input_signal <= 5)
```

Ogma generates the following Copilot specification:

```haskell
import Copilot.Compile.C99
import Copilot.Language hiding (prop)
import Copilot.Language.Prelude
import Copilot.Library.LTL (next)
import Copilot.Library.MTL hiding (since, alwaysBeen, trigger)
import Copilot.Library.PTLTL (since, previous, alwaysBeen)
import Language.Copilot (reify)
import Prelude hiding ((&&), (||), (++), not, (<=), (>=), (<), (>))
input_signal :: Stream Double
input_signal = extern "input_signal" Nothing
-- | propTestCopilot_001
-- @
-- test_component shall satisfy (input_signal <= 5)
-- @
propTestCopilot_001 :: Stream Bool
propTestCopilot_001 = ( alwaysBeen (( ( ( input_signal <= 5 ) ) )) )
-- | Complete specification. Calls the C function void handler(); when
-- the property is violated.
spec :: Spec
spec = do
trigger "handlerpropTestCopilot_001" (not propTestCopilot_001) []
main :: IO ()
main = reify spec >>= compile "fret"
```

This program can be compiled using Copilot to generate a `fret.c` file that
includes a hard real-time C99 implementation of the monitor. The specification
generated by FRET for the FRETish requirement shown above is included with the
Ogma distribution, and can be tested with:

```sh
$ ogma fret-component-spec --cocospec --fret-file-name examples/fret-reqs-small.json > FretCopilot.hs
$ runhaskell FretCopilot.hs
```

The first step executes `ogma`, generating a Copilot monitor in a file called
`FretCopilot.hs`. The second step executes the Copilot compiler, generating a C
implementation `fret.c` and C header file `fret.h`.

The resulting `fret.c` file can be tested with the main provided in
`examples/fret-reqs-small-main.c`, which defines a handler for Copilot to call
when the property monitored is violated, and a main function that steps through
the execution, providing new data for the Copilot monitor:

```c
#include <stdio.h>
double input_signal; // Input data made available for the monitor
void step(void); // Copilot monitor's main entry point
void handlerpropTestCopilot_001(void) {
printf("Monitor condition violated\n");
}
int main (int argc, char** argv) {
int i = 0;
input_signal = 0;
for (i=0; i<10; i++) {
printf("Running step %d\n", i);
input_signal += 1;
step();
}
return 0;
}
```
To compile both files, run `gcc examples/fret-reqs-small-main.c fret.c -o
main`. Executing the resulting `main` shows that the condition is violated
after a number of steps:
```
Running step 0
Running step 1
Running step 2
Running step 3
Running step 4
Running step 5
Monitor condition violated
Running step 6
Monitor condition violated
Running step 7
Monitor condition violated
Running step 8
Monitor condition violated
Running step 9
Monitor condition violated
```
Take a peek inside the intermediate files `FretCopilot.hs`, `fret.c` and
`fret.h` to see what is being generated by Ogma and by Copilot.
The generated C code can be integrated as part of a larger application. For
example, the following shows a Copilot monitor generated from a FRET file
integrated in an X-Plane widget that presents information to users during a
flight in the X-Plane simulator.
<p align="center">
<img src="https://raw.githubusercontent.com/nasa/ogma/develop/docs/xplane.png" width="75%">
<br />
<sup><i>Screenshot of Copilot monitor generated by Ogma from FRET requirement,
integrated into the X-Plane flight simulator. The widget on the right side of
the screen presents information received and returned by the monitor, with a
red/fire icon to signal that the monitor has been triggered (i.e., that the
property has been violated).</i></sup>
</p>
**Numeric Representations**
FRET Component Specifications use the types `real` and `int` to represent
different numeric variables. Copilot distinguishes between different numeric
representations and supports multiple precisions, and so does the final C
code generated from the Copilot specification.
To help users generate code that works as part of a larger system without
modifications, Ogma includes two additional flags to map the types `real` and
`int` to specific Copilot (Haskell) types. For example, the following command
would generate a Copilot specification for a hypothetical
`numeric-example.json` FRET CS file while mapping all real variables to the
type `Double` and all integer variables to the type `Int32`:
```
$ ogma fret-component-spec --fret-file-name numeric-example.json --map-int-to Int32 --map-real-to Double
```
In the name of flexibility, Ogma does not sanitize the values of these
variables and copies the types passed to these options verbatim to the
generated Copilot code. It is the user's responsibility to ensure the types
passed are valid Haskell types within the scope of the module generated.
Note that Copilot supports only a limited subset of numeric types, which
must be instances of the type class
[`Typed`](https://hackage.haskell.org/package/copilot-core/docs/Copilot-Core-Type.html#t:Typed).
**Name customization**
All FRET-related commands allow for customization of the target C filenames via
an argument `--target-file-name`. For example, the following execution causes
the C files produced by Copilot to be called `monitor.c`, `monitor.h` and
`monitor_types.h`, as opposed to the default names `fret.c`, `fret.h` and
`fret_types.h`, respectively:
```sh
$ ogma fret-component-spec --cocospec --fret-file-name examples/fret-reqs-small.json --target-file-name monitor > FretCopilot.hs
$ runhaskell FretCopilot.hs
$ ls monitor*
monitor.c monitor.h monitor_types.h
```
The main invocation of `ogma` with `--help` lists sub-commands available. More
details are provided in the following sections.

## cFS Application Generation

Expand Down Expand Up @@ -415,28 +196,20 @@ the data needed by the monitors and report any violations. At present, support
for ROS app generation is considered preliminary.
ROS applications are generated using the Ogma command `ros`, which receives
five main arguments:
four main arguments:
- `--app-target-dir DIR`: location where the ROS application files must be
stored.
- `--fret-file-name FILENAME`: a file containing a FRET component specification.
- `--variable-file FILENAME`: a file containing a list of variables that must
be made available to the monitor.
- `--variable-db FILENAME`: a file containing a database of known variables,
and the topic they are included with.
- `--handlers FILENAME`: a file containing a list of handlers used in the
specification.
Not all arguments are mandatory. You should always provide either a FRET
component specification, or both a variable file and a handlers file. If you
provide a variables file or a handler file _and_ a FRET component
specification, the variables/handlers file will always take precedence, and the
variables/requirements listed in the FRET component specification file will be
ignored.
The following execution generates an initial ROS application for runtime
monitoring using Copilot:
```sh
$ ogma ros --fret-file-name Export.json --variable-file variables --variable-db ros-variable-db --app-target-dir ros_demo
$ ogma ros --handlers filename --variable-file variables --variable-db ros-variable-db --app-target-dir ros_demo
```

The application generated by Ogma contains the following files:
Expand Down Expand Up @@ -475,25 +248,17 @@ F' components are generated using the Ogma command `fprime`, which receives
five main arguments:
- `--app-target-dir DIR`: location where the F' application files must be
stored.
- `--fret-file-name FILENAME`: a file containing a FRET component specification.
- `--variable-file FILENAME`: a file containing a list of variables that must
be made available to the monitor.
- `--variable-db FILENAME`: a file containing a database of known variables,
and their types.
- `--handlers FILENAME`: a file containing a list of handlers used in the
specification.

Not all arguments are mandatory. You should always provide either a FRET
component specification, or both a variable file and a handlers file. If you
provide a variables file or a handler file _and_ a FRET component
specification, the variables/handlers file will always take precedence, and the
variables/requirements listed in the FRET component specification file will be
ignored.
The following execution generates an initial F' component for runtime
monitoring using Copilot:
```sh
$ ogma fprime --fret-file-name Export.json --variable-db fprime-variable-db --app-target-dir fprime_demo
$ ogma fprime --handlers filename --variable-file filename --variable-db fprime-variable-db --app-target-dir fprime_demo
```

The component generated by Ogma contains the following files:
Expand All @@ -506,19 +271,6 @@ fprime_demo/Dockerfile
fprime_demo/inline-copilot
```

For completion, the following execution should compile the produced monitoring
component in a docker environment (assuming that the necessary `Export.json`,
`fprime-variable-db` files exist, they have consistent information, etc.) using
FPrime's Reference Application:
```sh
$ ogma fprime --fret-file-name Export.json --variable-db fprime-variable-db --app-target-dir fprime_demo
$ ogma fret-component-spec --fret-file-name Export.json --target-file-name copilot > Spec.hs
$ cd fprime_demo/
$ runhaskell ../Spec.hs
$ docker build -t fprime .
```
### File formats

The format of the variables, variable DB, and handlers file are as follows.
Expand All @@ -536,8 +288,8 @@ pullup

The variables database file contains a list of known variables and their types.
It does not matter if there are variables that are not used for one particular
specification, FRET file, or requirement/monitor. The only thing that matters
is that the variables used, and their types, be listed in the file. Continuing
specification, or property/requirement/monitor. The only thing that matters is
that the variables used, and their types, be listed in the file. Continuing
with the same example, we could have:

```sh
Expand All @@ -559,13 +311,6 @@ $ cat handlers
handlerpropREQ_001
```

Note that the handler name must match the one used by Copilot. Ogma transforms
requirement names to ensure that they corresponding handlers are valid C
identifiers. For example, the Ogma-generated monitor for a FRET requirement
`REQ_001` would, upon violation, call a C handler `handlerpropREQ_001`. The
transformation only applies if you are working with FRET files and not directly
with other source languages.
### Current limitations

The user must place the code generated by Copilot monitors in three files,
Expand Down Expand Up @@ -632,12 +377,9 @@ changes.

Ogma has been created by Ivan Perez and Alwyn Goodloe.

The Ogma team would like to thank Dimitra Giannakopoulou, Anastasia Mavridou,
and Thomas Pressburger, from the FRET Team at NASA Ames, for the continued
input during the development of Ogma.
We would also like to thank Cesar Munoz and Swee Balachandran, for their help
with the cFS backend.
The Ogma team would like to thank Swee Balachandran, Dimitra Giannakopoulou,
Anastasia Mavridou, Cesar Munoz and Thomas Pressburger, for the input during
the development of Ogma.

X-Plane images obtained via the X-Plane 10 (Pro) flight simulator. Re-shared
with permission.
Expand Down

0 comments on commit 5d07b72

Please sign in to comment.