Layer2_MMS_SW_SPARK: Reorganize F_FC behavior

UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

@@ -42,6 +42,8 @@ ACTIVITIES:
       A. Additional assumption: Translated into types (validity of inputs).
       6.6.3.1
       A. Additional guarantee: Translated as a postcondition.
+      6.6.4
+      Behavioural Specification: Mostly translated as contracts. Parts involving calculations or update frequencies have been kept as comments. Notably missing, external and internal disturbances (linked to weather conditions and AV behavior).
 
     - MMS.F_PT.F_EM:
       6.8.3.1
@@ -61,6 +63,15 @@ ACTIVITIES:
       7.3.2:
       Guarantees A, B: Not tranlated (linked to weather conditions)
 
+    - MMS.F_FC:
+      6.7.3.1:
+      Assumption A: Not tranlated (linked to measurements)
+      Assumption B: Input safety assumptions are automatic
+      Assumption C: Not translated, F_FC does not have the necessary inputs.
+      6.7.3.2:
+      Guarantees A, B, C: Not translated (linked to weather conditions and mechanical body behavior)
+      Guarantees D, E: Translated as postconditions.
+
   * 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 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.

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

+with MMS.F_PT.F_FC.State;
+
 package body MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
 
    procedure Run is
    begin
-      MMS.F_PT.F_FC.Behavior.Run;
+      Update_State;
+
+      if Mission_State in FLIGHT | LANDING then
+         Propulsion_Braking_Mutual_Exclusion;
+
+         Reference_Trajectory_Computation;
+         Gain_Scheduling;
+
+         if Engine_State = PROPULSION then
+            Propulsion_Control;
+            State.Braking_Torque := 0.0;
+         elsif Engine_State = BRAKING then
+            Braking_Control;
+            State.Propulsion_Torque := 0.0;
+         else
+            State.Braking_Torque := 0.0;
+            State.Propulsion_Torque := 0.0;
+         end if;
+      end if;
    end Run;
 
 end MMS.F_PT.F_FC.Behavior.Guarantees;

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

@@ -15,10 +15,12 @@ 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 = FLIGHT and then Engine_State in Braking_State_Type);
+     (Mission_State in FLIGHT | LANDING
+      and then Engine_State in Braking_State_Type);
 
    function Engine_State_In_Propulsion return Boolean is
-     (Mission_State = FLIGHT and then Engine_State in Propulsion_State_Type);
+     (Mission_State in FLIGHT | LANDING
+      and then Engine_State in Propulsion_State_Type);
 
    -----------------------------------
    -- High-Level Garantees for F_FC --
@@ -40,6 +42,7 @@ package MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
 
      and then
        (if Mission_State = ABORTED and then Mission_State'Old /= ABORTED
+           and then Aborted_With_Propulsion_Available
         then Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time);
 
 end MMS.F_PT.F_FC.Behavior.Guarantees;

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

@@ -9,53 +9,51 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    -- Inputs --
    ------------
 
-   function P return Distance_Type with Global => Private_State;
-   function P_Dot return Speed_Type with Global => Private_State;
-   function Q return Angle_Type with Global => Private_State;
+   function P return Distance_Type with Global => Input_State;
+   function P_Dot return Speed_Type with Global => Input_State;
+   function Q return Angle_Type with Global => Input_State;
 
    function Start_Take_Off return Boolean with
-     Global => Private_State,
+     Global => (Input => Input_State, Proof_In => Private_State),
      Pre    => Mission_State = INIT;
 
    function Start_Landing return Boolean with
-     Global => Private_State,
+     Global => (Input => Input_State, Proof_In => Private_State),
      Pre    => Mission_State = FLIGHT;
 
    function Operating_Point return Operating_Point_Type with
-     Global => Private_State;
+     Global => Input_State;
+
+   function Emergency_Landing return Boolean with
+     Global => Input_State;
 
    --------------------------
    -- Properties on Inputs --
    --------------------------
 
    function Operating_Point_Changed return Boolean with
-     Global => Private_State;
+     Global => Input_State;
 
    ----------------------
    -- Estimated Values --
    ----------------------
 
-   function Q_Dot return Speed_Type with Global => Private_State;
+   function Q_Dot return Speed_Type with Global => Input_State;
 
    ------------
    -- States --
    ------------
 
-   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 = FLIGHT;
-
-   type Engine_State_Type is
-     (PROPULSION, WAITING_BRAK, BRAKING, WAITING_PROP);
-
    function Engine_State return Engine_State_Type with
+     Global => (Input => Mutual_Exclusion_State, Proof_In => Private_State),
+     Pre    => Mission_State in FLIGHT | LANDING;
+
+   function Aborted_With_Propulsion_Available return Boolean with
      Global => Private_State,
-     Pre    => Mission_State = FLIGHT;
+     Pre    => Mission_State = ABORTED;
 
    ----------------
    -- Properties --
@@ -63,8 +61,12 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
 
    --  From 6.7.3.2
 
+   function Flight_Phase return Flight_Phase_Type with
+     Global => (Input => Trajectory_State, Proof_In => Private_State),
+     Pre    => Mission_State = FLIGHT;
+
    function In_Safety_Envelope return Boolean is
-     (case Flight_Phase_State is
+     (case Flight_Phase is
          when CLIMB   =>
             Q_Dot in MMS.F_PT.F_FC.Data.Qdot_MinCl .. MMS.F_PT.F_FC.Data.Qdot_MaxCl
               and Q < MMS.F_PT.F_FC.Data.Q_MaxCl,
@@ -77,28 +79,30 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
               and Q < MMS.F_PT.F_FC.Data.Q_MaxDs)
    with Pre => Mission_State = FLIGHT;
 
-   function Time_Since_In_Safety_Escape return Time_Type with
+   function Already_Running return Boolean with
      Global => Private_State,
+     Pre    => Mission_State in FLIGHT | LANDING;
+
+   function Time_Since_In_Safety_Escape return Time_Type with
+     Global => (Input    => Private_State,
+                Proof_In => (Input_State, Trajectory_State)),
      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,
+     Global => (Input    => Private_State,
+                Proof_In => (Input_State, Trajectory_State)),
      Pre    => Mission_State = FLIGHT and then not In_Safety_Envelope;
 
    function Time_Since_Stopped return Time_Type with
-     Global => Private_State,
-     Pre    => Mission_State = FLIGHT;
-
-   -------------
-   -- Outputs --
-   -------------
+     Global => (Input => Mutual_Exclusion_State, Proof_In => Private_State),
+     Pre    => Mission_State in FLIGHT | LANDING;
 
    function Propulsion_Torque return Torque_Type with
-     Global => Private_State;
+     Global => (Input => Propulsion_State, Proof_In => Private_State);
 
    function Braking_Torque return Torque_Type with
-     Global => Private_State;
+     Global => (Input => Braking_State, Proof_In => Private_State);
 
    ---------------------------------------
    -- Behavioural Specification of F_FC --
@@ -106,46 +110,64 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
 
    procedure Read_Inputs with
    --  Read values of inputs once and for all and update the current state
-     Global => (In_Out => Private_State,
-                Input  => External.State),
+
      Post   => Operating_Point_Changed =
        (Operating_Point'Old /= Operating_Point);
 
    procedure Write_Outputs with
    --  Compute values of outputs from the current state
-     Global => (Input  => Private_State,
+
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Mutual_Exclusion_State,
+                           Gain_Scheduling_State,
+                           Propulsion_State,
+                           Braking_State),
                 Output => Output_State);
 
-   procedure Run with
-     Global         => (In_Out => Private_State),
+   procedure Update_State with
+     Global         => (Input  => (Input_State, Trajectory_State),
+                        In_Out => Private_State),
      Contract_Cases =>
 
        --  ??? All these are guesses...
 
-       (Mission_State = INIT
+       ((Mission_State in INIT .. LANDING)
+        and then Emergency_Landing
+        =>
+          Mission_State = ABORTED
+        and then not Aborted_With_Propulsion_Available,
+
+        Mission_State = INIT
+        and then not Emergency_Landing
         and then Start_Take_Off
         =>
-          Mission_State = FLIGHT
-        and then Engine_State = PROPULSION,
+          Mission_State = FLIGHT,
 
         Mission_State = INIT
+        and then not Emergency_Landing
         and then not Start_Take_Off
         =>
           Mission_State = INIT,
 
         Mission_State = FLIGHT
+        and then not Emergency_Landing
         and then Start_Landing
         =>
           Mission_State = LANDING,
 
         Mission_State = FLIGHT
+        and then not Emergency_Landing
         and then not Start_Landing
         =>
           (if Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time then
                Mission_State = ABORTED
+             and then Aborted_With_Propulsion_Available
            else Mission_State = FLIGHT),
 
         Mission_State = LANDING
+        and then not Emergency_Landing
         =>
           (if P_Dot = 0.0 and then Q_Dot = 0.0 then
                Mission_State = COMPLETE
@@ -156,12 +178,9 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
           Mission_State = Mission_State'Old),
 
      Post           =>
-
-       --  Changes in the operating point provoque termination of the current
-       --  cruise phase and activate a transient climb or descent phase to
-       --  capture the new operating point (see 6.6.4 4. Cruise).
-
-       (if Operating_Point_Changed then Flight_Phase_State in CLIMB | DESCENT)
+       (if Mission_State in FLIGHT | LANDING then
+          Engine_State = Engine_State'Old  -- ??? Needed due to current limitation in proof tool
+        and then Already_Running = (Mission_State'Old in FLIGHT | LANDING))
 
        --  Time_Since_In_Safety_Escape is the number of seconds since the first
        --  occurrence of safety escapes.
@@ -169,51 +188,128 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
      and then
        (if not In_Safety_Envelope then
           (if In_Safety_Envelope'Old then Time_Since_In_Safety_Escape = 0
-           else Time_Since_In_Safety_Escape > Time_Since_In_Safety_Escape'Old))
-
-        --  6.7.4 Propulsion braking mutual exclusion
+           else Time_Since_In_Safety_Escape > Time_Since_In_Safety_Escape'Old));
 
-       and then
-       (if Mission_State = FLIGHT and then Mission_State'Old = FLIGHT then
-          (case Engine_State'Old is
-           when PROPULSION   =>
-             (if not In_Safety_Envelope
+   function Go_To_Braking return Boolean is
+     (Mission_State = LANDING
+      or else
+        (not In_Safety_Envelope
          and then
            (Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
-                 or else Fast_Evolving_Safety_Escape)
-              then Engine_State = WAITING_BRAK
-                and then Time_Since_Stopped = 0
-              else Engine_State = PROPULSION),
-
-           when BRAKING      =>
-             (if In_Safety_Envelope
-              then Engine_State = WAITING_PROP
-                and then Time_Since_Stopped = 0
-              else Engine_State = BRAKING),
-
-           when WAITING_PROP =>
-             (if not In_Safety_Envelope
-              and then (Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
-                        or else Fast_Evolving_Safety_Escape)
-              then Engine_State = BRAKING
-              elsif Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
+            or else Fast_Evolving_Safety_Escape)))
+   with
+     Pre    => Mission_State in FLIGHT | LANDING;
+
+   function Go_To_Propulsion return Boolean is
+     (Mission_State = FLIGHT and then In_Safety_Envelope)
+   with
+     Pre    => Mission_State in FLIGHT | LANDING;
+
+   procedure Propulsion_Braking_Mutual_Exclusion with
+     Global => (Input  => (Input_State, Trajectory_State, Private_State),
+                In_Out => Mutual_Exclusion_State),
+     Pre    => Mission_State in FLIGHT | LANDING,
+     Contract_Cases =>
+       (not Already_Running
+        =>
+          Engine_State = PROPULSION,
+
+        --  6.7.4 Propulsion braking mutual exclusion
+
+        Already_Running
+        and then Engine_State = PROPULSION
+        and then Go_To_Braking
+        =>
+          Engine_State = WAITING_BRAK
+        and then Time_Since_Stopped = 0,
+
+        Already_Running
+        and then Engine_State = PROPULSION
+        and then not Go_To_Braking
+        =>
+          Engine_State = PROPULSION,
+
+        Already_Running
+        and then Engine_State = BRAKING
+        and then Go_To_Propulsion
+        =>
+          Engine_State = WAITING_PROP
+        and then Time_Since_Stopped = 0,
+
+        Already_Running
+        and then Engine_State = BRAKING
+        and then not Go_To_Propulsion
+        =>
+          Engine_State = BRAKING,
+
+        Already_Running
+        and then Engine_State = WAITING_PROP
+        and then Go_To_Braking
+        =>
+          Engine_State = BRAKING,
+
+        Already_Running
+        and then Engine_State = WAITING_PROP
+        and then not Go_To_Braking
+        =>
+          (if Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
            then Engine_State = PROPULSION
            else Engine_State = WAITING_PROP
              and then Time_Since_Stopped > Time_Since_Stopped'Old),
 
-           when WAITING_BRAK =>
-               (if In_Safety_Envelope
-                then Engine_State = PROPULSION
-                elsif Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
+        Already_Running
+        and then Engine_State = WAITING_BRAK
+        and then Go_To_Propulsion
+        =>
+          Engine_State = PROPULSION,
+
+        Already_Running
+        and then Engine_State = WAITING_BRAK
+        and then not Go_To_Propulsion
+        =>
+          (if 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);
+   procedure Reference_Trajectory_Computation with
+     Global => (Input  => (Input_State, Private_State),
+                In_Out => Trajectory_State),
+     Pre    => Mission_State in FLIGHT .. LANDING,
+     Post   =>
+
+       --  Changes in the operating point provoque termination of the current
+       --  cruise phase and activate a transient climb or descent phase to
+       --  capture the new operating point (see 6.6.4 4. Cruise).
+
+       (if Mission_State = FLIGHT and then Operating_Point_Changed then
+          Flight_Phase in CLIMB | DESCENT);
+
+   procedure Gain_Scheduling with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Mutual_Exclusion_State),
+                In_Out => Gain_Scheduling_State),
+     Pre    => Mission_State in FLIGHT .. LANDING;
+
+   procedure Propulsion_Control with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Gain_Scheduling_State,
+                           Mutual_Exclusion_State),
+                In_Out => Propulsion_State),
+     Pre    => Mission_State = FLIGHT and then Engine_State = PROPULSION;
+
+   procedure Braking_Control with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Gain_Scheduling_State,
+                           Mutual_Exclusion_State),
+                In_Out => Braking_State),
+     Pre    => Mission_State in FLIGHT .. LANDING
+     and then Engine_State = BRAKING;
 
 end MMS.F_PT.F_FC.Behavior;

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

@@ -40,4 +40,7 @@ package MMS.F_PT.F_FC.Input is
    function Mission_Range return Current_Range_Type
      renames MMS.F_PT.F_MM.Output.Mission_Range; 
    
+   function Emergency_Landing return Boolean 
+     renames MMS.F_PT.F_MM.Output.Emergency_Landing;
+
 end MMS.F_PT.F_FC.Input;

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

+private
+package MMS.F_PT.F_FC.State is
+
+   Propulsion_Torque : Torque_Type with Part_Of => Propulsion_State;
+
+   Braking_Torque : Torque_Type with Part_Of => Braking_State;
+
+end MMS.F_PT.F_FC.State;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads

 with Types; use Types;
 
-package MMS.F_PT.F_FC with Abstract_State => (Private_State, Output_State) is
+package MMS.F_PT.F_FC with
+  Abstract_State => (Input_State,
+                     Trajectory_State,
+                     Private_State,
+                     Mutual_Exclusion_State,
+                     Gain_Scheduling_State,
+                     Propulsion_State,
+                     Braking_State,
+                     Output_State)
+is
    pragma Elaborate_Body (MMS.F_PT.F_FC);
 
    type Flight_Cell_Center_Type is record
@@ -25,4 +34,9 @@ package MMS.F_PT.F_FC with Abstract_State => (Private_State, Output_State) is
 
    type Time_Type is new Integer; --  in s ??? some bounds
 
+   type Mission_State_Type is (INIT, FLIGHT, LANDING, ABORTED, COMPLETE);
+
+   type Engine_State_Type is
+     (PROPULSION, WAITING_BRAK, BRAKING, WAITING_PROP);
+
 end MMS.F_PT.F_FC;

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

@@ -41,12 +41,14 @@ package body MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
 
                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;

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

@@ -14,9 +14,9 @@ package MMS.F_PT.F_MM.Output is
    
    function Ready_For_Takeoff return Boolean with Global => Output_State;
    
-   -------------
-   -- To F_EL --
-   --------------
+   ----------------------
+   -- To F_EL and F_CM --
+   ----------------------
 
    function Emergency_Landing return Boolean with Global => Output_State;