From 5d07b72237ffe7330a6704de31e394e1c10425aa Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 18 Jan 2024 14:31:09 +0000 Subject: [PATCH 1/2] ogma-cli: Structure README around backends. Refs #75. 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. --- ogma-cli/README.md | 292 +++------------------------------------------ 1 file changed, 17 insertions(+), 275 deletions(-) diff --git a/ogma-cli/README.md b/ogma-cli/README.md index 1c89919..b008a05 100644 --- a/ogma-cli/README.md +++ b/ogma-cli/README.md @@ -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. - - -

- Conversion of requirements into C code -
- Conversion of FRET requirements into C code. -

-

Monitoring within simulation video
@@ -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) @@ -98,215 +86,8 @@ After that, the `ogma` executable will be placed in the directory # Usage [(Back to top)](#table-of-contents) -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 -[(Back to top)](#table-of-contents) - -[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). - -

- -
-Screenshot of requirement specified inside NASA's requirements elicitation tool FRET. -

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

- -
-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). -

- -**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 @@ -415,10 +196,9 @@ 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, @@ -426,17 +206,10 @@ 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: @@ -475,7 +248,6 @@ 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, @@ -483,17 +255,10 @@ 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: @@ -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. @@ -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 @@ -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, @@ -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. From 41ef5b5f31fe4be8de06b4b2c8935eb10e0f1c01 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Thu, 18 Jan 2024 14:35:17 +0000 Subject: [PATCH 2/2] ogma-cli: Document changes in CHANGELOG. Refs #75. --- ogma-cli/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index cc5b594..126a4ef 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-cli +## [1.X.Y] - 2024-01-18 + +* Re-structure README around on backends (#75). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112).