Layer2_MMS_SW_SPARK: Split functional behavior of F_MM in distinct parts

UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

@@ -30,7 +30,7 @@ ACTIVITIES:
  2 - Review of the specification for translatability in Ada contracts:
 
   * Design:
-    Each component provides a Run procedure located in a child package Comp.Behavior. This procedure is responsible from updating the internal state of the component at each step. Scheduling, as well as handling of inputs and outputs are not considered here. The procedure Run may have a contract, representing the part of its behavioural specification which is translatable into Ada contracts. Contracts from the specification document are stored in a distinct unit, named Comp.Behavior.Guarantees. Parts of specification contracts and of functional behaviours which are not fit for translation into SPARK contracts will be listed here.
+    Each component provides one or more procedures located in a child package Comp.Behavior. They are responsible of updating the internal state of the component at each step. Scheduling is not considered here. These procedures may have a contract, representing the part of behavioural specification of the component which is translatable into Ada contracts. Contracts from the specification document are translated as Ada contracts of a Run procedure located in a distinct unit, named Comp.Behavior.Guarantees. Parts of specification contracts and of functional behaviours which are not fit for translation into SPARK contracts will be listed here.
 
   * Report for translatability into Ada contracts:
     - MMS.F_PT.F_MM:
@@ -55,7 +55,7 @@ ACTIVITIES:
       Assumptions A. B, C, E: Not translated (linked with AV's electrical and mechanical behavior)
       6.9.3.2:
       Guarantees A, B: Not translated
-      Guaranted C: Not translated (arbitration has been moved from F_CM)
+      Guarantee C: Translated as a postcondition on F_MM.Behavior.garantees.Run (arbitration has been moved to F_MM).
 
     - MMS.F_EL:
       7.3.2:
@@ -63,6 +63,6 @@ ACTIVITIES:
 
   * Verifications:
     The SPARK toolset can be used to check that:
-    - Ada contracts are consistent. If it is a case by case contract, SPARK can check that all cases are covered and that no two cases can apply to the same inputs. If some properties or some information can only be checked in some cases, these cases can be expressed as preconditions on property or information functions and SPARK will check that they are always used in valid context.
+    - Ada contracts are consistent. If it is a case by case contract, SPARK can check that all cases are covered and that no two cases can apply to the same inputs. If some properties or some information can only be accessed in some cases, these cases can be expressed as preconditions on property or information functions and SPARK will check that they are always used in valid context.
 
-    - Guarantees are implied by the behavioral specification. If both can be expressed as Ada contracts, SPARK can check that, if the behavioural specification of a component is respected by its implementation, then the implementation will also respect the guarantees as stated in the specification contracts.
+    - Guarantees are implied by the behavioral specification. If both can be expressed as Ada contracts, SPARK can check that, if the behavioural specification of a component is respected by its implementation, then the implementation will also respect the guarantees as stated in the specification contracts. For this, a body has to be provided for Behavior.garantees.Run, calling explicitely the procedures declared in Behavior in a meaningful order.

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.ads

@@ -15,10 +15,10 @@ package MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
    range BRAKING .. WAITING_PROP;
 
    function Engine_State_In_Braking return Boolean is
-     (Mission_State = RUNNING and then Engine_State in Braking_State_Type);
+     (Mission_State = FLIGHT and then Engine_State in Braking_State_Type);
 
    function Engine_State_In_Propulsion return Boolean is
-     (Mission_State = RUNNING and then Engine_State in Propulsion_State_Type);
+     (Mission_State = FLIGHT and then Engine_State in Propulsion_State_Type);
 
    -----------------------------------
    -- High-Level Garantees for F_FC --

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior.ads

@@ -19,7 +19,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
 
    function Start_Landing return Boolean with
      Global => Private_State,
-     Pre    => Mission_State = RUNNING;
+     Pre    => Mission_State = FLIGHT;
 
    function Operating_Point return Operating_Point_Type with
      Global => Private_State;
@@ -41,21 +41,21 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    -- States --
    ------------
 
-   type Mission_State_Type is (INIT, RUNNING, ABORTED, COMPLETE);
+   type Mission_State_Type is (INIT, FLIGHT, LANDING, ABORTED, COMPLETE);
 
    function Mission_State return Mission_State_Type with
      Global => Private_State;
 
    function Flight_Phase_State return Flight_Phase_Type with
      Global => Private_State,
-     Pre    => Mission_State = RUNNING;
+     Pre    => Mission_State = FLIGHT;
 
    type Engine_State_Type is
      (PROPULSION, WAITING_BRAK, BRAKING, WAITING_PROP);
 
    function Engine_State return Engine_State_Type with
      Global => Private_State,
-     Pre    => Mission_State = RUNNING;
+     Pre    => Mission_State = FLIGHT;
 
    ----------------
    -- Properties --
@@ -75,20 +75,30 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
          when DESCENT =>
             Q_Dot in MMS.F_PT.F_FC.Data.Qdot_MinDs .. MMS.F_PT.F_FC.Data.Qdot_MaxDs
               and Q < MMS.F_PT.F_FC.Data.Q_MaxDs)
-   with Pre => Mission_State = RUNNING;
+   with Pre => Mission_State = FLIGHT;
 
    function Time_Since_In_Safety_Escape return Time_Type with
      Global => Private_State,
-     Pre    => (Mission_State = RUNNING and then not In_Safety_Envelope)
+     Pre    => (Mission_State = FLIGHT and then not In_Safety_Envelope)
      or else Mission_State = ABORTED;
 
    function Fast_Evolving_Safety_Escape return Boolean with
      Global => Private_State,
-     Pre    => Mission_State = RUNNING and then not In_Safety_Envelope;
+     Pre    => Mission_State = FLIGHT and then not In_Safety_Envelope;
 
    function Time_Since_Stopped return Time_Type with
      Global => Private_State,
-     Pre    => Mission_State = RUNNING;
+     Pre    => Mission_State = FLIGHT;
+
+   -------------
+   -- Outputs --
+   -------------
+
+   function Propulsion_Torque return Torque_Type with
+     Global => Private_State;
+
+   function Braking_Torque return Torque_Type with
+     Global => Private_State;
 
    ---------------------------------------
    -- Behavioural Specification of F_FC --
@@ -115,7 +125,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
        (Mission_State = INIT
         and then Start_Take_Off
         =>
-          Mission_State = RUNNING
+          Mission_State = FLIGHT
         and then Engine_State = PROPULSION,
 
         Mission_State = INIT
@@ -123,17 +133,23 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
         =>
           Mission_State = INIT,
 
-        Mission_State = RUNNING
+        Mission_State = FLIGHT
         and then Start_Landing
         =>
-          Mission_State = COMPLETE,
+          Mission_State = LANDING,
 
-        Mission_State = RUNNING
+        Mission_State = FLIGHT
         and then not Start_Landing
         =>
           (if Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time then
                Mission_State = ABORTED
-           else Mission_State = RUNNING),
+           else Mission_State = FLIGHT),
+
+        Mission_State = LANDING
+        =>
+          (if P_Dot = 0.0 and then Q_Dot = 0.0 then
+               Mission_State = COMPLETE
+           else Mission_State = LANDING),
 
         (Mission_State in COMPLETE | ABORTED)
         =>
@@ -158,7 +174,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
         --  6.7.4 Propulsion braking mutual exclusion
 
        and then
-       (if Mission_State = RUNNING and then Mission_State'Old = RUNNING then
+       (if Mission_State = FLIGHT and then Mission_State'Old = FLIGHT then
           (case Engine_State'Old is
            when PROPULSION   =>
              (if not In_Safety_Envelope
@@ -191,6 +207,13 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
                 elsif Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
                 then Engine_State = BRAKING
                 else Engine_State = WAITING_BRAK
-                  and then Time_Since_Stopped > Time_Since_Stopped'Old)));
+                  and then Time_Since_Stopped > Time_Since_Stopped'Old)))
+
+     and then
+       (if Mission_State = FLIGHT and then Engine_State /= PROPULSION then
+          Propulsion_Torque = 0.0)
+     and then
+       (if Mission_State = FLIGHT and then Engine_State /= BRAKING then
+          Braking_Torque = 0.0);
 
 end MMS.F_PT.F_FC.Behavior;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.adb

@@ -2,9 +2,67 @@ with Types; use Types;
 
 package body MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
 
+   Initial_Energy_Test_Done   : Boolean with Ghost;
+   In_Flight_Energy_Test_Done : Boolean with Ghost;
+   Energy_Test_Succeded       : Boolean with Ghost;
+
+   function Initial_Energy_Test_Succeeded return Boolean is
+     (Initial_Energy_Test_Done and then Energy_Test_Succeded);
+
+   function In_Flight_Energy_Test_Failed return Boolean is
+     (In_Flight_Energy_Test_Done and then not Energy_Test_Succeded);
+
    procedure Run is
    begin
-      MMS.F_PT.F_MM.Behavior.Run;
+      Initial_Energy_Test_Done := False;
+      In_Flight_Energy_Test_Done := False;
+      Energy_Test_Succeded := False;
+
+      Read_Inputs;
+
+      if Power_On then
+         Management_Of_Navigation_Modes_Options_Parameters;
+
+         if Power_State = On then
+            if On_State in INIT | RUNNING
+              and then Mission_Parameters_Defined
+            then
+               Operating_Point_Update_Management;
+            end if;
+
+            if (On_State = RUNNING
+                and then Running_State = FLIGHT
+                and then Current_Flight_Phase = CRUISE)
+              or else
+                (On_State = INIT
+                 and then Init_Completed)
+            then
+               Mission_Viability_Logic;
+
+               if On_State = RUNNING then
+                  In_Flight_Mission_Viability_Logic;
+                  In_Flight_Energy_Test_Done := True;
+                  Energy_Test_Succeded :=
+                    In_Flight_Energy_Compatible_With_Mission;
+
+               else
+                  Initial_Mission_Viability_Logic;
+                  Initial_Energy_Test_Done := True;
+                  Energy_Test_Succeded :=
+                    Initial_Energy_Compatible_With_Mission;
+               end if;
+
+            elsif On_State = RUNNING
+              and then Running_State = FLIGHT
+              and then Current_Flight_Phase = DESCENT
+            then
+               Mission_Termination_Control;
+            end if;
+         end if;
+      end if;
+
+      Update_States;
+      Write_Outputs;
    end Run;
 
 end MMS.F_PT.F_MM.Behavior.Guarantees;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.ads

---  This package provides a wrapper above MMS.F_PT.F_MM.Behavior.Run which
---  is used to verify in SPARK that high level guarantees on F_MM are implied
---  by its behavioural specification.
+--  This package provides a Run procedure which simulates execution of the
+--  main loop of F_MM and is used to verify in SPARK that high level guarantees
+--  on F_MM are implied by its behavioural specification.
 
 with Types; use Types;
 
@@ -14,11 +14,13 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
    function In_Take_Off_State return Boolean is
       (Power_State = On
        and then On_State = RUNNING
-       and then Running_State = TAKE_OFF);
+       and then Running_State = TAKE_OFF)
+   with Global => Private_State;
 
    function Mission_Aborted return Boolean is
       (Power_State = On
-       and then On_State = ABORTED);
+       and then On_State = ABORTED)
+   with Global => Private_State;
 
    function Mission_Cancelled return Boolean is
       (Power_State = On
@@ -26,6 +28,10 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
        and then Init_State = CANCELLED)
    with Global => Private_State;
 
+   function Initial_Energy_Test_Succeeded return Boolean with Ghost;
+
+   function In_Flight_Energy_Test_Failed return Boolean with Ghost;
+
    -----------------------------------
    -- High-Level Garantees for F_MM --
    -----------------------------------
@@ -37,16 +43,14 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
       --  incompatible with mission completion.
 
       (if In_Take_Off_State and then not In_Take_Off_State'Old then
-         Initial_Energy_Compatible_With_Mission)
+         Initial_Energy_Test_Succeeded)
 
       --  6.6.3.B Any mission cancellation is signaled to CP and GS.
 
       and then
-       (if Mission_Aborted and then not Mission_Aborted'Old then
-           Mission_Aborted_Signaled)
+       (if Mission_Aborted then Mission_Aborted_Signaled)
       and then
-       (if Mission_Cancelled and then not Mission_Cancelled'Old then
-           Mission_Cancelled_Signaled)
+       (if Mission_Cancelled then Mission_Cancelled_Signaled)
 
       --  6.6.3.2.A Missions cancelled for energy reasons can be proven
       --  infeasible.
@@ -54,6 +58,18 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
       and then
        (if Mission_Aborted and then not Mission_Aborted'Old
           and then Aborted_For_Energy_Reasons
-        then not In_Flight_Energy_Compatible_With_Mission);
+        then In_Flight_Energy_Test_Failed)
+
+      --  6.9.3.2.C When A mode is set on CP, the navigation options/parameters
+      --  are that of USB key or initialization is not complete.
+
+      and then
+       (if Power_On
+          and then Navigation_Mode_From_CP = A
+          and then Mission_Parameters_Defined
+        then
+          USB_Key_Present
+        and then Operating_Mode = Operating_Mode_From_CP
+        and then Navigation_Parameters = Navigation_Parameters_From_USB_Key);
 
 end MMS.F_PT.F_MM.Behavior.Guarantees;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-state.ads

@@ -48,22 +48,53 @@ package MMS.F_PT.F_MM.State is
    -- Private_State --
    -------------------
 
-   Navigation_Mode : Navigation_Mode_Type with Part_Of => Private_State;
+   Power_State : Power_State_Type with Part_Of => Private_State;
 
-   Operating_Mode : Navigation_Option_Type with Part_Of => Private_State;
+   On_State : On_State_Type with Part_Of => Private_State;
+
+   Init_State : Init_State_Type with Part_Of => Private_State;
+
+   Running_State : Running_State_Type with Part_Of => Private_State;
+
+   Aborted_For_Energy_Reasons : Boolean with Part_Of => Private_State;
+
+   --------------------------------
+   -- Navigation_Parameter_State --
+   --------------------------------
+
+   Navigation_Mode : Navigation_Mode_Type with
+     Part_Of => Navigation_Parameter_State;
+
+   Operating_Mode : Navigation_Option_Type with
+     Part_Of => Navigation_Parameter_State;
 
    Navigation_Parameters : Navigation_Parameters_Type with
-     Part_Of => Private_State;
+     Part_Of => Navigation_Parameter_State;
+
+   ---------------------------
+   -- Operating_Point_State --
+   ---------------------------
+
+   Mission_Range  : Current_Range_Type with Part_Of => Operating_Point_State;
 
-   Operating_Point : Operating_Point_Type with Part_Of => Private_State;
+   Operating_Point : Operating_Point_Type with
+     Part_Of => Operating_Point_State;
+
+   ---------------------------
+   -- Viability_Logic_State --
+   ---------------------------
 
    Initial_Energy_Compatible_With_Mission : Boolean with
-     Part_Of => Private_State;
+     Part_Of => Viability_Logic_State;
 
    In_Flight_Energy_Compatible_With_Mission : Boolean with
-     Part_Of => Private_State;
+     Part_Of => Viability_Logic_State;
+
+   -------------------------------
+   -- Mission_Termination_State --
+   -------------------------------
 
-   Descent_Over : Boolean with Part_Of => Private_State;
+   Descent_Over : Boolean with Part_Of => Mission_Termination_State;
 
    ------------------
    -- Output_State --

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb

 with MMS.F_PT.F_MM.State; use MMS.F_PT.F_MM.State;
 package body MMS.F_PT.F_MM with
-  SPARK_Mode,
-  Refined_State => (Input_State   => (Input_Navigation_Parameters,
+SPARK_Mode,
+  Refined_State => (Input_State   =>
+                      (Input_Navigation_Parameters,
                        Input_Navigation_Mode,
                        Input_Navigation_Option,
                        Input_Go,
@@ -18,7 +19,8 @@ package body MMS.F_PT.F_MM with
                        Input_Current_Altitude,
                        Input_Current_Flight_Phase,
                        Input_Energy_Level),
-                    Output_State  => (Output_Mission_Cancelled,
+                    Output_State  =>
+                      (Output_Mission_Cancelled,
                        Output_Mission_Complete,
                        Output_Mission_Aborted,
                        Output_Emergency_Landing,
@@ -27,12 +29,23 @@ package body MMS.F_PT.F_MM with
                        Output_Operating_Point,
                        Output_Operating_Mode,
                        Output_Mission_Range),
-                    Private_State => (Navigation_Mode,
+                    Private_State =>
+                      (Power_State,
+                       On_State,
+                       Init_State,
+                       Running_State,
+                       Aborted_For_Energy_Reasons),
+                    Navigation_Parameter_State =>
+                      (Navigation_Mode,
                        Operating_Mode,
-                                      Navigation_Parameters,
-                                      Operating_Point,
-                                      Initial_Energy_Compatible_With_Mission,
-                                      In_Flight_Energy_Compatible_With_Mission,
-                                      Descent_Over))
+                       Navigation_Parameters),
+                    Operating_Point_State =>
+                      (Mission_Range,
+                       Operating_Point),
+                    Viability_Logic_State =>
+                      (Initial_Energy_Compatible_With_Mission,
+                       In_Flight_Energy_Compatible_With_Mission),
+                    Mission_Termination_State =>
+                      (Descent_Over))
 is
 end MMS.F_PT.F_MM;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads

@@ -2,10 +2,25 @@ with Types; use Types;
 
 package MMS.F_PT.F_MM with
   SPARK_Mode,
-  Abstract_State => (Private_State, Output_State, Input_State)
+  Abstract_State =>
+    (Navigation_Parameter_State,
+     Operating_Point_State,
+     Viability_Logic_State,
+     Mission_Termination_State,
+     Private_State,
+     Output_State,
+     Input_State)
 is
    pragma Elaborate_Body (MMS.F_PT.F_MM);
 
+   type Power_State_Type is (ON, OFF);
+
+   type On_State_Type is (INIT, RUNNING, COMPLETE, ABORTED);
+
+   type Running_State_Type is (TAKE_OFF, FLIGHT, LANDING);
+
+   type Init_State_Type is (PREPARATION, READY, CANCELLED);
+
    type Viability_Cell_Center_Type is record
       Distance     : Current_Range_Type;
       Altitude     : Current_Altitude_Type;
@@ -48,7 +63,22 @@ is
       Distance        : Mission_Profile_Distance_Type;
    end record;
 
-   type Neighbour_Mission_Profile_Array_Type is array (Positive range 1 .. 16)
+   type Num_Of_Neighbours is new Positive range 1 .. 16;
+
+   type Neighbour_Mission_Profile_Array_Type is array
+     (Num_Of_Neighbours range <>)
      of Neighbour_Mission_Profile_Type;
 
+   type Neighbour_Mission_Profiles (Size : Num_Of_Neighbours) is record
+     Neighbours : Neighbour_Mission_Profile_Array_Type (1 .. Size);
+   end record;
+
+   type Energy_Level_Array_Type is array
+     (Num_Of_Neighbours range <>)
+     of Energy_Level_Type;
+
+   type Energy_Levels (Size : Num_Of_Neighbours) is record
+     Neighbours : Energy_Level_Array_Type (1 .. Size);
+   end record;
+
 end MMS.F_PT.F_MM;