Skip to content

Commit

Permalink
ogma-cli: Document fprime command in README. Refs #77.
Browse files Browse the repository at this point in the history
Add instructions of how the `fprime` command works.

Add entry in list of features documenting the new F' (FPrime) support.

Describe existing limitations for the command.
  • Loading branch information
ivanperez-keera committed Mar 21, 2023
1 parent caa0c3e commit 59308e0
Showing 1 changed file with 119 additions and 0 deletions.
119 changes: 119 additions & 0 deletions ogma-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,9 @@ verification framework that generates hard real-time C99 code.
- 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">
Expand All @@ -45,6 +48,7 @@ verification framework that generates hard real-time C99 code.
- [cFS Application Generation](#cfs-application-generation)
- [Struct Interface Generation](#struct-interface-generation)
- [ROS Application Generation](#ros-application-generation)
- [F' Application Generation](#f-application-generation)
- [Contributions](#contributions)
- [Acknowledgements](#acknowledgements)
- [License](#license)
Expand Down Expand Up @@ -108,6 +112,7 @@ 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 FPrime 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
Expand Down Expand Up @@ -442,6 +447,120 @@ be generated for any variables for which a DB entry cannot be found. At present,
Ogma will proceed without warnings if a variable is mentioned in a requirement
or variables file but a matching entry is not found in the variable DB.

## F' Component Generation

F' (FPrime) is a component-based framework for spaceflight applications.

Ogma is able to generate F' monitoring components that subscribe to obtain
the data needed by the monitors and report any violations. At present, support
for F' component generation is considered preliminary.

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
```

The component generated by Ogma contains the following files:
```
fprime_demo/CMakeLists.txt
fprime_demo/Copilot.fpp
fprime_demo/Copilot.cpp
fprime_demo/Copilot.hpp
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 > Spec.hs
$ sed -i -e 's/compile "fret"/compile "copilot"/g' 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.

The variables file can contain a list of variables used in a specification, one
per line. For example, if we are working with a specification that uses three
boolean variables called `autopilot`, `sensorLimitsExceeded`, and `pullup`, we
can provide them to Ogma's `fprime` command in a file like the following:
```sh
$ cat variables
autopilot
sensorLimitsExceeded
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
with the same example, we could have:

```sh
$ cat fprime-variable-db
("temperature", "uint8_t")
("autopilot", "bool")
("sensorLimitsExceeded", "bool")
("pullup", "bool")
("current_consumption", "float")
```

In our example, we only care about the boolean variables; it is sufficient that
they be listed in the variable DB file.

Finally, the handlers file is a list of monitor handlers that the generated
FPrime component should restrict to monitoring. They are listed one per line:
```sh
$ 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,
`fprime_demo/src/copilot.h`, `fprime_demo/src/copilot_types.h` and
`fprime_demo/src/copilot.c`. No Copilot or C code for the monitors is generated
by default by the `fprime` command.

The code generated by default assumes that handlers receive no arguments. The
user must modify the handlers accordingly if that is not the case.

## Struct Interface Generation

A lot of the information that must be monitored in real-world C applications is
Expand Down

0 comments on commit 59308e0

Please sign in to comment.