Merge branch 'develop-cfs' into develop. Close #3.

ogma-cli/README.md

@@ -11,6 +11,12 @@ verification framework that generates hard real-time C99 code.
   FRET](https://github.com/NASA-SW-VnV/fret) into corresponding monitors in
   Copilot.
 
+- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) applications
+  that use Copilot for monitoring data received from the message bus.
+
+- 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.
 
 ## Table of Contents
@@ -20,6 +26,7 @@ verification framework that generates hard real-time C99 code.
   - [Compilation](#compilation)
 - [Usage](#usage)
   - [Language Transformations: FRET](#language-transformations-fret)
+  - [cFS Application Generation](#cfs-application-generation)
   - [Struct Interface Generation](#struct-interface-generation)
 - [Contributions](#contributions)
 - [Acknowledgements](#acknowledgements)
@@ -82,6 +89,8 @@ Available options:
 
 Available commands:
   structs                  Generate Copilot structs from C structs
+  handlers                 Generate message handlers from C structs
+  cfs                      Generate a complete cFS/Copilot application
   fret-component-spec      Generate a Copilot file from a FRET Component
                            Specification
   fret-reqs-db             Generate a Copilot file from a FRET Requirements
@@ -208,6 +217,99 @@ 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.
 
+## cFS Application Generation
+
+Ogma includes multiple facilities to generate NASA's core Flight System
+(cFS) applications. The cFS applications generated by Ogma perform three
+simple steps to connect Copilot monitors to cFS:
+- Subscribe to a message in the cFS communication bus.
+- When a message of the desired kind arrives, copy the data to make it
+  available to Copilot and call the monitor's main entry point.
+- Declare handlers that are executed when the property being monitored is
+  violated.
+
+When using this facility, Ogma produces a Copilot file that the user is
+expected to modify to implement the property to monitor. To avoid having to
+modify the generated C files that implement the cFS app itself, Ogma gives the
+ability to state what information one is interested in monitoring. If the kind
+of information is known to Ogma, it will automatically subscribe to the
+necessary messages and make it available to Copilot. Ogma provides additional
+flags to customize the list of known variables, so that projects can maintain
+their own variable databases beyond what Ogma includes by default.
+
+cFS applications are generated using the Ogma command `cfs`, which receives
+three main arguments:
+- `--app-target-dir DIR`: location where the cFS application files must be
+  stored.
+- `--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 message they are included with.
+
+The following execution generates an initial cFS application for runtime
+monitoring using Copilot:
+```
+$ ogma cfs --variable-db examples/cfs-variable-db --variable-file examples/cfs-variables
+```
+
+The application generated by Ogma contains the following files:
+```
+copilot-cfs-demo/CMakeLists.txt
+copilot-cfs-demo/fsw/for_build/Makefile
+copilot-cfs-demo/fsw/mission_inc/copilot_cfs_perfids.h
+copilot-cfs-demo/fsw/platform_inc/copilot_cfs_msgids.h
+copilot-cfs-demo/fsw/src/copilot_cfs.c
+copilot-cfs-demo/fsw/src/Properties.hs
+copilot-cfs-demo/fsw/src/copilot_cfs_msg.h
+copilot-cfs-demo/fsw/src/copilot_cfs_events.h
+copilot-cfs-demo/fsw/src/copilot_cfs_version.h
+copilot-cfs-demo/fsw/src/copilot_cfs.h
+```
+
+Users are expected to modify `Properties.hs` to adjust the property being
+monitored. Although it is possible to adjust the file `copilot_cfs.c` to
+include property violation handlers, we recommend adding them in a separate C
+file and modifying the compilation scripts to include that additional file.
+That way, invoking Ogma again will not overwrite the changes made to the cFS
+application.
+
+In this particular example, the C code generated contains the following
+instruction to subscribe to an `ICAROUS_POSITION_MID` message to obtain
+the vehicle position:
+```c
+    CFE_SB_Subscribe(ICAROUS_POSITION_MID, COPILOT_CommandPipe);
+```
+
+The message dispatcher included in the application detects a message
+of this kind and calls a dedicated subroutine:
+```c
+void COPILOT_ProcessCommandPacket(void)
+{
+    CFE_SB_MsgId_t  MsgId;
+
+    MsgId = CFE_SB_GetMsgId(COPILOTMsgPtr);
+
+    switch (MsgId)
+    {
+        case ICAROUS_POSITION_MID:
+            COPILOT_ProcessIcarousPosition();
+            break;
+    ...
+```
+
+Finally, the dedicated subroutine makes data available to the monitor
+and calls the main Copilot entry point `step`:
+
+```c
+void COPILOT_ProcessIcarousPosition(void)
+{
+    position_t* msg;
+    msg = (position_t*) COPILOTMsgPtr;
+    position = *msg;
+    step();
+}
+```
+
 ## Struct Interface Generation
 
 A lot of the information that must be monitored in real-world C applications is
@@ -262,6 +364,9 @@ 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.
+
 # License
 <sup>[(Back to top)](#table-of-contents)</sup>
 

ogma-cli/examples/cfs-variable-db

@@ -0,0 +1,2 @@
+("position", "position_t", "ICAROUS_POSITION_MID", "IcarousPosition")
+("velocity", "velocity_t", "ICAROUS_VELOCITY_MID", "IcarousVelocity")

ogma-cli/examples/cfs-variables

@@ -0,0 +1 @@
+position

ogma-cli/ogma-cli.cabal

@@ -57,6 +57,15 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      - Generating the glue code necessary to work with C
                        structs in Copilot.
                      .
+                     - Generating
+                       <https://cfs.gsfc.nasa.gov/ NASA Core Flight System>
+                       applications that use Copilot for monitoring data
+                       received from the message bus.
+                     .
+                     - Generating message handlers for NASA Core Flight System
+                       applications to make external data in structs available
+                       to a Copilot monitor.
+                     .
                      The main invocation with @--help@ lists sub-commands available.
                      .
                      >$ ogma --help
@@ -70,6 +79,8 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      >
                      >Available commands:
                      >  structs                  Generate Copilot structs from C structs
+                     >  handlers                 Generate message handlers from C structs
+                     >  cfs                      Generate a complete CFS/Copilot application
                      >  fret-component-spec      Generate a Copilot file from a FRET Component
                      >                           Specification
                      >  fret-reqs-db             Generate a Copilot file from a FRET Requirements
@@ -83,6 +94,8 @@ description:         Ogma is a tool to facilitate the integration of safe runtim
                      .
                      - <https://github.com/NASA-SW-VnV/fret The FRET repository>.
                      .
+                     - <https://cfs.gsfc.nasa.gov/ The NASA Core Flight System web page>.
+                     .
                      - <https://ntrs.nasa.gov/citations/20200003164 "Copilot 3">, Perez, Dedden and Goodloe. 2020.
                      .
                      - <https://shemesh.larc.nasa.gov/people/cam/publications/FMAS2020_3.pdf "From Requirements to Autonomous Flight">, Dutle et al. 2020.
@@ -93,7 +106,9 @@ executable ogma
     Main.hs
 
   other-modules:
+    CLI.CommandCFSApp
     CLI.CommandCStructs2Copilot
+    CLI.CommandCStructs2MsgHandlers
     CLI.CommandFretComponentSpec2Copilot
     CLI.CommandFretReqsDB2Copilot
     CLI.CommandTop

ogma-cli/src/CLI/CommandCFSApp.hs

@@ -0,0 +1,117 @@
+-- Copyright 2020 United States Government as represented by the Administrator
+-- of the National Aeronautics and Space Administration. All Rights Reserved.
+--
+-- Disclaimers
+--
+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
+-- IT "AS IS."
+--
+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
+-- AGREEMENT.
+--
+-- | CLI interface to the CFSApp subcommand.
+module CLI.CommandCFSApp
+    (
+      -- * Direct command access
+      command
+    , CommandOpts
+    , ErrorCode
+
+      -- * CLI
+    , commandDesc
+    , commandOptsParser
+    )
+  where
+
+-- External imports
+import Options.Applicative ( Parser, help, long, metavar, optional, showDefault,
+                             strOption, value )
+
+-- External imports: command results
+import Command.Result ( Result )
+
+-- External imports: actions or commands supported
+import Command.CFSApp ( ErrorCode, cFSApp )
+
+-- * Command
+
+-- | Options needed to generate the cFS application.
+data CommandOpts = CommandOpts
+  { cFSAppTarget   :: String
+  , cFSAppVarNames :: String
+  , cFSAppVarDB    :: Maybe String
+  }
+
+-- | Create <https://cfs.gsfc.nasa.gov/ NASA core Flight System> (cFS)
+-- applications that subscribe to the communication bus and call Copilot when
+-- new messages arrive.
+--
+-- This is just an uncurried version of "Command.CFSApp".
+command :: CommandOpts -> IO (Result ErrorCode)
+command c =
+  cFSApp (cFSAppTarget c) (cFSAppVarNames c) (cFSAppVarDB c)
+
+-- * CLI
+
+-- | cFS command description
+commandDesc :: String
+commandDesc = "Generate a complete cFS/Copilot application"
+
+-- | Subparser for the @cfs@ command, used to generate a NASA Core Flight
+-- System application connected to Copilot monitors.
+commandOptsParser :: Parser CommandOpts
+commandOptsParser = CommandOpts
+  <$> strOption
+        (  long "app-target-dir"
+        <> metavar "DIR"
+        <> showDefault
+        <> value "copilot-cfs-demo"
+        <> help strCFSAppDirArgDesc
+        )
+  <*> strOption
+        (  long "variable-file"
+        <> metavar "FILENAME"
+        <> showDefault
+        <> value "variables"
+        <> help strCFSAppVarListArgDesc
+        )
+  <*> optional
+        ( strOption
+            (  long "variable-db"
+            <> metavar "FILENAME"
+            <> help strCFSAppVarDBArgDesc
+            )
+        )
+
+-- | Argument target directory to cFS app generation command
+strCFSAppDirArgDesc :: String
+strCFSAppDirArgDesc = "Target directory"
+
+-- | Argument variable list to cFS app generation command
+strCFSAppVarListArgDesc :: String
+strCFSAppVarListArgDesc =
+  "File containing list of cFS/ICAROUS variables to make accessible"
+
+-- | Argument variable database to cFS app generation command
+strCFSAppVarDBArgDesc :: String
+strCFSAppVarDBArgDesc =
+  "File containing a DB of known cFS/ICAROUS variables"

ogma-cli/src/CLI/CommandCStructs2MsgHandlers.hs

@@ -0,0 +1,85 @@
+-- Copyright 2020 United States Government as represented by the Administrator
+-- of the National Aeronautics and Space Administration. All Rights Reserved.
+--
+-- Disclaimers
+--
+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY
+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE
+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF
+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN
+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR
+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR
+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,
+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING
+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES
+-- IT "AS IS."
+--
+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS
+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN
+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,
+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S
+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE
+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY
+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY
+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS
+-- AGREEMENT.
+--
+-- | CLI interface to the CStructs2Copilot subcommand
+module CLI.CommandCStructs2MsgHandlers
+    (
+      -- * Direct command access
+      command
+    , CommandOpts
+    , ErrorCode
+
+      -- * CLI
+    , commandDesc
+    , commandOptsParser
+    )
+  where
+
+-- External imports
+import Options.Applicative ( Parser, help, long, metavar, strOption )
+
+-- External imports: command results
+import Command.Result ( Result )
+
+-- External imports: actions or commands supported
+import Command.CStructs2MsgHandlers ( ErrorCode, cstructs2MsgHandlers )
+
+-- * Command
+
+-- | Options to generate message handlers from C struct definitions.
+newtype CommandOpts = CommandOpts
+  { msgHandlersFileName :: FilePath }
+
+-- | Generate C methods that process NASA Core Flight System messages dealing
+-- with the structs defined in a header file.
+--
+-- This is just an uncurried version of "Command.CStructs2MsgHandlers".
+command :: CommandOpts -> IO (Result ErrorCode)
+command c = cstructs2MsgHandlers (msgHandlersFileName c)
+
+-- * CLI
+
+-- | Command description for CLI help.
+commandDesc :: String
+commandDesc = "Generate message handlers from C structs"
+
+-- | Subparser for the @handlers@ command, used to generate message handers
+-- from C structs.
+commandOptsParser :: Parser CommandOpts
+commandOptsParser = CommandOpts
+  <$> strOption
+        (  long "header-file-name"
+        <> metavar "FILENAME"
+        <> help strMsgHandlersHeaderArgDesc
+        )
+
+-- | Argument C header file to handler generation command
+strMsgHandlersHeaderArgDesc :: String
+strMsgHandlersHeaderArgDesc = "C header file with struct definitions"