diff --git a/ogma-cli/README.md b/ogma-cli/README.md index ffa09d2..dc0f565 100644 --- a/ogma-cli/README.md +++ b/ogma-cli/README.md @@ -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. +

Conversion of requirements into C code @@ -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) @@ -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 @@ -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