Merge branch 'develop-fret' into develop. Close #2.

ogma-cli/README.md

@@ -7,6 +7,10 @@ verification framework that generates hard real-time C99 code.
 
 # Features
 
+- Translating requirements defined in [NASA requirements elicitation tool
+  FRET](https://github.com/NASA-SW-VnV/fret) into corresponding monitors in
+  Copilot.
+
 - Generating the glue code necessary to work with C structs in Copilot.
 
 ## Table of Contents
@@ -15,6 +19,7 @@ verification framework that generates hard real-time C99 code.
   - [Pre-requisites](#pre-requisites)
   - [Compilation](#compilation)
 - [Usage](#usage)
+  - [Language Transformations: FRET](#language-transformations-fret)
   - [Struct Interface Generation](#struct-interface-generation)
 - [Contributions](#contributions)
 - [Acknowledgements](#acknowledgements)
@@ -77,8 +82,132 @@ Available options:
 
 Available commands:
   structs                  Generate Copilot structs from C structs
+  fret-component-spec      Generate a Copilot file from a FRET Component
+                           Specification
+  fret-reqs-db             Generate a Copilot file from a FRET Requirements
+                           Database
+```
+
+## Language transformations: FRET
+<sup>[(Back to top)](#table-of-contents)</sup>
+
+Ogma can convert specifications written in other languages to Copilot monitors,
+such as the ones supported by [NASA's requirements elicitation tool
+FRET](https://github.com/NASA-SW-VnV/fret). 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 based on Lustre. Ogma uses the SMV expressions by
+default, but the CLI flag `--cocospec` can be used to select the CoCoSpec
+variant of requirements instead.
+
+For 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 FRET
+specification example 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
+$ cabal v1-exec -- 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.
+
 ## Struct Interface Generation
 
 A lot of the information that must be monitored in real-world C applications is
@@ -126,6 +255,13 @@ The best way to contribute to Ogma is to report any issues you find via the
 issue tracker, and to use Ogma to build applications or in your own research
 and let us know about your results.
 
+# Acknowledgements
+<sup>[(Back to top)](#table-of-contents)</sup>
+
+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.
+
 # License
 <sup>[(Back to top)](#table-of-contents)</sup>
 

ogma-cli/examples/DB.json

@@ -0,0 +1,45 @@
+[
+ {
+     "reqid": "TEST",
+     "parent_reqid": "",
+     "project": "STALLUSECASE",
+     "rationale": "Trivial requirement",
+     "comments": "Trivial requirement for testing purposes",
+     "fulltext": "external_component shall satisfy (external_signal <= 35)",
+     "semantics": {
+         "type": "nasa",
+         "scope": {
+             "type": "null"
+         },
+         "condition": "null",
+         "timing": "null",
+         "response": "satisfaction",
+         "variables": {
+             "regular": [
+                 "external_signal"
+             ],
+             "modes": []
+         },
+         "component_name": "external_component",
+         "componentTextRange": [
+             0,
+             17
+         ],
+         "post_condition": "(( external_signal <= 35 ))",
+         "responseTextRange": [
+             25,
+             55
+         ],
+         "ft": "((! LAST) U <b><i>(( external_signal <= 35 ))</i></b>)",
+         "pt": "(O <b><i>(( external_signal <= 35 ))</i></b>)",
+         "ftExpanded": "((! LAST) U <b><i>(( external_signal <= 35 ))</i></b>)",
+         "ptExpanded": "(O(external_signal))",
+         "component": "<b><i>external_component</i></b>",
+         "CoCoSpecCode": "(O(external_signal <= 35))",
+         "diagramVariables": "Response = <b><i>(( external_signal <= 35 ))</i></b>.",
+         "description": "ENFORCED: in the interval defined by the entire execution.\nTRIGGER: first point in the interval.\nREQUIRES: for every trigger, RES must hold at some time point between (and including) the trigger and the end of the interval.",
+         "diagram": "_media/user-interface/examples/svgDiagrams/null_null_null_satisfaction.svg"
+     },
+     "_id": "51a1bc60-c3d0-11eb-a339-fd36e7b31a1f"
+ }
+]

ogma-cli/examples/fret-reqs-full.json

@@ -0,0 +1,19 @@
+{
+  "RTSASpec": {
+    "Internal_variables": [],
+    "Other_variables": [
+      {"name":"param_is_short", "type":"bool"},
+      {"name":"param_value_short", "type":"real"},
+      {"name":"param_value_long", "type":"real"},
+      {"name":"upper_param_limit", "type":"real"},
+      {"name":"lower_param_limit", "type":"real"},
+      {"name":"envelope_issue", "type":"bool"}
+    ],
+    "Requirements": [
+      {
+        "name": "behnazOne",
+        "CoCoSpecCode": "(H(((( ( param_is_short and ( ( ( param_value_short * 1048576 ) >= upper_param_limit ) or ( ( param_value_short * 1048576 ) <= lower_param_limit ) ) ) or ( not param_is_short and ( ( ( param_value_long * 1048576 ) >= upper_param_limit ) or ( ( param_value_long * 1048576 ) <= lower_param_limit ) ) ) )) and ((pre ( not (( ( param_is_short and ( ( ( param_value_short * 1048576 ) >= upper_param_limit ) or ( ( param_value_short * 1048576 ) <= lower_param_limit ) ) ) or ( not param_is_short and ( ( ( param_value_long * 1048576 ) >= upper_param_limit ) or ( ( param_value_long * 1048576 ) <= lower_param_limit ) ) ) )))) or FTP)) => (envelope_issue)))"
+      }
+    ]
+  }
+}

ogma-cli/examples/fret-reqs-small-main.c

@@ -0,0 +1,21 @@
+#include <stdio.h>
+
+double input_signal;
+void step(void);
+
+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;
+}

ogma-cli/examples/fret-reqs-small.json

@@ -0,0 +1,22 @@
+{
+  "test_componentSpec": {
+    "Functions": [
+    ],
+    "Internal_variables": [
+    ],
+    "Other_variables": [
+      {
+        "name": "input_signal",
+        "type": "Double"
+      }
+    ],
+    "Requirements": [
+      {
+        "CoCoSpecCode": "(O((( input_signal <= 5 ))))",
+        "fretish": "test_component shall satisfy (input_signal <= 5)",
+        "name": "testCopilot-001",
+        "ptLTL": "(O (( input_signal <= 5 )))"
+      }
+    ]
+  }
+}

ogma-cli/examples/fret-reqs.json

@@ -0,0 +1,66 @@
+[
+    {
+        "reqid": "test_req1",
+        "parent_reqid": "",
+        "project": "Test",
+        "rationale": "",
+        "fulltext": "during flight_mode when conflict_detected planner_module shall within 10 seconds satisfy (replanning_mode).",
+        "semantics": {
+            "type": "nasa",
+            "scope": {
+                "type": "in"
+            },
+            "condition": "regular",
+            "timing": "within",
+            "response": "satisfaction",
+            "variables": {
+                "regular": [
+                    "conflict_detected",
+                    "replanning_mode"
+                ],
+                "modes": [
+                    "flight_mode"
+                ]
+            },
+            "scope_mode": "flight_mode",
+            "scopeTextRange": [
+                0,
+                17
+            ],
+            "regular_condition": "(conflict_detected)",
+            "qualifier_word": "when",
+            "pre_condition": "(conflict_detected)",
+            "conditionTextRange": [
+                19,
+                40
+            ],
+            "component_name": "planner_module",
+            "componentTextRange": [
+                42,
+                55
+            ],
+            "duration": [
+                "10"
+            ],
+            "timingTextRange": [
+                63,
+                79
+            ],
+            "post_condition": "(( replanning_mode ))",
+            "responseTextRange": [
+                81,
+                105
+            ],
+            "ft": "((LAST V ((! (Fin_<b><i>flight_mode</i></b> & (! LAST))) | (X (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))",
+            "pt": "((H ((Lin_<b><i>flight_mode</i></b> & (! FTP)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))) & (((! Lin_<b><i>flight_mode</i></b>) S ((! Lin_<b><i>flight_mode</i></b>) & Fin_<b><i>flight_mode</i></b>)) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))",
+            "ftExpanded": "((LAST V ((! ((((! <b><i>flight_mode</i></b>) & (! LAST)) & (X <b><i>flight_mode</i></b>)) & (! LAST))) | (X (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))",
+            "ptExpanded": "((H ((((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>)) & (Y TRUE)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))) & (((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) S ((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))",
+            "component": "<b><i>planner_module</i></b>",
+            "CoCoSpecCode": "((H(((( not flight_mode) and (pre (flight_mode))) and ( not FTP)) => (pre (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))) and ((SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ( not (( not flight_mode) and (pre (flight_mode)))) )) => (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))",
+            "diagramVariables": "M = <b><i>flight_mode</i></b>, TC = <b><i>(conflict_detected)</i></b>,  n = <b><i>10</i></b>, Response = <b><i>(( replanning_mode ))</i></b>.",
+            "description": "ENFORCED: in every interval where <b><i>flight_mode</i></b> holds.\nTRIGGER: first point in the interval if <b><i>(conflict_detected)</i></b> is true and any point in the interval where <b><i>(conflict_detected)</i></b> becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=<b><i>10</i></b> from the trigger, except if the end of the interval occurs sooner.",
+            "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_within_satisfaction.svg"
+        },
+        "_id": "fbc0a840-a04b-11ea-b135-098996762962"
+    }
+]