reorg

big reorganization agreed during 2017-10-26
2025-11-30 21:27:58 +01:00 · 2017-10-26 15:28:50 +02:00
parent c55d46c6a8
commit b914e6c263
169 changed files with 41455 additions and 41498 deletions
--- a/UseCaseData/Layer2_MMS_SW_SPARK/DESIGN.txt
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/DESIGN.txt
@@ -0,0 +1,79 @@
+ACTIVITIES:
+ 1 - Identification and validation of inputs / outputs:
+
+  * Design:
+    The specification is structured into a component based architecture. Each component and sub-component has identified inputs and outputs, which may have types, bounds... Information flows through these signals between components.
+    Each sub-component is a child package of its container. Inputs and outputs of components are translated as functions without parameters stored in specific child packages named Comp.Input and Comp.Output. Types for signals are stored at the root of the architecture, namely in mms.ads. They are as precise as we could make them, based on the specifications available.
+    Links between inputs and outputs of various components are made through renamings, or through expression functions when the mapping is more complex. Inputs and outputs are grouped together depending on where they are coming from/where they are going to.
+
+  * Verifications:
+    We have checked by review that:
+    - Inputs and outputs of components are consistent, namely, if a component A has an output to another component B, then B must have an input from A and conversely.
+      + Method: If a function F is in a group of inputs (resp. outputs) of a component Comp1 labelled 'From Comp2' (resp. 'To Comp2'), where Comp2 is inside the same container as Comp1, check that Comp2.Output (resp. Comp2.Input) has a section 'To Comp1' (resp. 'From Comp1') containing a matching output (resp. input).
+
+      + Result: Inconsistencies have been reported.
+
+    - Types (as well as bounds and units) are consistent between sources and destinations.
+      + Method: This is enforced through static typing by turning the destination of a signal as a renaming of its origin.
+
+      + Assumptions: When no information was supplied, we have made the following choices:
+        * Payload_Mass_Type is in kg with a precision of 0.1 and bounds of 1.0 and 5.0.
+        * [...]
+
+    - The component structure is well-formed, namely, information does not flow through the edge of components.
+      + Method: This can be verified by reviewing use clauses inserted at the beginning of inputs or outputs packages. More precisely
+        * An input package Comp.Subcomp.Input can only reference outputs of siblings Comp.*.Output or inputs of parent Comp.Input.
+        * An output package Comp.Output can only reference its own inputs Comp.Input or outputs of its children Comp.Subcomp.Output.
+
+      + Result: No inconsistency found.
+
+ 2 - Review of the specification for translatability in Ada contracts:
+
+  * Design:
+    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:
+      6.6.3
+      Inherited assumptions A, B, C, D, E: Not translated (linked to weather condition).
+      Inherited assumption F: Translated into types (validity of inputs).
+      Inherited guarantees A, B: Translated as postconditions.
+      6.6.3.1
+      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
+      Assumptions A, B: Not translated (linked with AV, mechanical body behavior)
+      6.8.3.2
+      Guarantee A: Not translated (linked with weather conditions)
+      Guarantees B, C: Not translated (linked with actual embedded energy which is not measurable)
+
+    - MMS.F_PT.F_CM:
+      6.9.3.1:
+      Assumptions A. B, C, E: Not translated (linked with AV's electrical and mechanical behavior)
+      6.9.3.2:
+      Guarantees A, B: The outputs are ensured to be initialized
+      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:
+      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.
+
+    - 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.
--- a/UseCaseData/Layer2_MMS_SW_SPARK/README.md
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/README.md
@@ -0,0 +1,2 @@
+This folder contains the SPARK version of the software layer development
+& assurance artefacts for the Mission Management subsystem
--- a/UseCaseData/Layer2_MMS_SW_SPARK/external.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/external.ads
@@ -0,0 +1,73 @@
+with Types; use Types;
+
+package External with Abstract_State => (State with External => Async_Writers) is
+
+   ------------------------------------------------------
+   -- Ground-based Mission Preparation and Supervision --
+   ------------------------------------------------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option with
+     Volatile_Function,
+     Global => State;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option with
+     Volatile_Function,
+     Global => State;
+
+   function Navigation_Option return Navigation_Option_Type_Option with
+     Volatile_Function,
+     Global => State;
+
+   function Go return Boolean with
+     Volatile_Function,
+     Global => State;
+
+   function Emergency_Landing return Boolean with
+     Volatile_Function,
+     Global => State;
+
+   --------------------------------------------------
+   -- AV-based Mission Preparation (Control Panel) --
+   --------------------------------------------------
+
+   function On_OFF_Push_Button return Boolean with
+     Volatile_Function,
+     Global => State;
+
+   function Start_Push_Button return Boolean with
+     Volatile_Function,
+     Global => State;
+
+   function Mode_Switch return Navigation_Mode_Type with
+     Volatile_Function,
+     Global => State;
+
+   function Bay_Switch return Bay_Switch_Type with
+     Volatile_Function,
+     Global => State;
+
+   function Payload_Mass return Payload_Mass_Type with
+     Volatile_Function,
+     Global => State;
+
+   function USB_Key return USB_Key_Type_Option with
+     Volatile_Function,
+     Global => State;
+
+   -------------------------
+   -- Physical Parameters --
+   -------------------------
+
+   function P return Distance_Type with
+     Volatile_Function,
+     Global => State;
+
+   function P_Dot return Speed_Type with
+     Volatile_Function,
+     Global => State;
+
+   function Q return Angle_Type with
+     Volatile_Function,
+     Global => State;
+
+end External;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-behavior.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-behavior.ads
@@ -0,0 +1,37 @@
+with Types; use Types;
+
+package MMS.F_EL.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;
+   
+   ----------------------
+   -- Estimated Values --
+   ----------------------
+
+   function Q_Dot return Speed_Type with Global => Private_State;
+   
+   ---------------------------------------
+   -- Behavioural Specification of F_EL --
+   ---------------------------------------
+
+   procedure Read_Inputs with
+   --  Read values of inputs once and for all and update the current state
+     Global => (In_Out => Private_State);
+
+   procedure Write_Outputs with
+   --  Compute values of outputs from the current state
+     Global => (Input  => Private_State,
+                Output => Output_State);
+
+   procedure Run with
+     Global => (In_Out => Private_State); 
+
+end MMS.F_EL.Behavior;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-input.ads
@@ -0,0 +1,28 @@
+with MMS.Input;
+with MMS.F_PT.Output;
+
+with Types; use Types;
+
+package MMS.F_EL.Input is
+
+   --------------
+   -- From MMS --
+   --------------
+
+   function P return Distance_Type
+     renames MMS.Input.P;
+
+   function P_Dot return Speed_Type
+     renames MMS.Input.P_Dot;
+   
+   function Q return Angle_Type
+     renames MMS.Input.Q;
+   
+   ---------------
+   -- From F_PT --
+   ---------------
+   
+   function Emergency_Landing return Boolean
+     renames MMS.F_PT.Output.Emergency_Landing;
+   
+end MMS.F_EL.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-output.ads
@@ -0,0 +1,19 @@
+with Types; use Types;
+
+package MMS.F_EL.Output is
+
+   ------------
+   -- To MMS --
+   ------------
+   
+   function Propulsion_Torque return Torque_Type with Global => Output_State;
+   
+   function Braking_Torque return Torque_Type with Global => Output_State;
+   
+   -------------
+   -- To F_PT --
+   -------------
+   
+   function Mission_Abort return Boolean with Global => Output_State;
+
+end MMS.F_EL.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-state.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-state.ads
@@ -0,0 +1,4 @@
+private
+package MMS.F_EL.State is
+
+end MMS.F_EL.State;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el.ads
@@ -0,0 +1,4 @@
+package MMS.F_EL with Abstract_State => (Private_State, Output_State) is
+   pragma Elaborate_Body (MMS.F_EL);
+
+end MMS.F_EL;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-data.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-data.ads
@@ -0,0 +1,7 @@
+with Types; use Types;
+
+package MMS.F_PT.Data is
+
+   Payload_Mass_Grid  : Payload_Mass_Grid_Type (1 .. 10); -- ??? bounds
+
+end MMS.F_PT.Data;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-input.ads
@@ -0,0 +1,92 @@
+with MMS.F_PT.Input;
+with MMS.F_PT.F_MM.Output;
+with MMS.F_PT.F_FC.Output;
+with MMS.F_PT.F_EM.Output;
+
+with Types; use Types;
+
+package MMS.F_PT.F_CM.Input is
+   
+   ---------------
+   -- From F_PT --
+   ---------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
+     renames MMS.F_PT.Input.Navigation_Parameters;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option
+     renames MMS.F_PT.Input.Navigation_Mode;
+   
+   function Navigation_Option return Navigation_Option_Type_Option
+     renames MMS.F_PT.Input.Navigation_Option;
+
+   function Go return Boolean
+     renames MMS.F_PT.Input.Go;   
+
+   function Emergency_Landing return Boolean
+     renames MMS.F_PT.Input.Emergency_Landing;
+
+   function On_OFF_Push_Button return Boolean
+     renames MMS.F_PT.Input.On_OFF_Push_Button;
+
+   function Start_Push_Button return Boolean
+     renames MMS.F_PT.Input.Start_Push_Button;
+
+   function Mode_Switch return Navigation_Mode_Type
+     renames MMS.F_PT.Input.Mode_Switch;
+
+   function Bay_Switch return Bay_Switch_Type
+     renames MMS.F_PT.Input.Bay_Switch; 
+
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.F_PT.Input.Payload_Mass;
+   
+   function USB_Key return USB_Key_Type_Option
+     renames MMS.F_PT.Input.USB_Key;
+   
+   function P return Distance_Type
+     renames MMS.F_PT.Input.P;
+   
+   function P_Dot return Speed_Type
+     renames MMS.F_PT.Input.P_Dot;
+   
+   function Q return Angle_Type
+     renames MMS.F_PT.Input.Q;
+   
+   ---------------
+   -- From F_MM --
+   ---------------
+   
+   function Mission_Aborted return Boolean 
+     renames MMS.F_PT.F_MM.Output.Mission_Aborted;
+   
+   function Mission_Complete return Boolean  
+     renames MMS.F_PT.F_MM.Output.Mission_Complete;
+   
+   function Mission_Cancelled return Boolean
+     renames MMS.F_PT.F_MM.Output.Mission_Cancelled;
+   
+   function Ready_For_Takeoff return Boolean
+     renames MMS.F_PT.F_MM.Output.Ready_For_Takeoff;
+   
+   ---------------
+   -- From F_EM --
+   ---------------
+   
+   function Primary_Source return Source_Type
+     renames MMS.F_PT.F_EM.Output.Primary_Source;
+   
+   function Secondary_Source return Source_Type
+     renames MMS.F_PT.F_EM.Output.Secondary_Source;
+   
+   ---------------
+   -- From F_FC --
+   ---------------
+   
+   function Propulsion_Torque return Torque_Type
+     renames MMS.F_PT.F_FC.Output.Propulsion_Torque;
+   
+   function Braking_Torque return Torque_Type
+     renames MMS.F_PT.F_FC.Output.Braking_Torque;
+   
+end MMS.F_PT.F_CM.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-output.ads
@@ -0,0 +1,109 @@
+with MMS.F_PT.F_CM.Input;
+
+with Types; use Types;
+
+package MMS.F_PT.F_CM.Output is
+
+   -------------
+   -- To F_PT --
+   -------------
+
+   function CP_Switches return CP_Switches_Type is
+     (CP_Switches_Type'
+        (Power      => MMS.F_PT.F_CM.Input.On_OFF_Push_Button, -- ???
+         Mode       => MMS.F_PT.F_CM.Input.Mode_Switch,
+         Bay        => MMS.F_PT.F_CM.Input.Bay_Switch,
+         Start      => MMS.F_PT.F_CM.Input.Start_Push_Button,
+         Rotactor_1 => 
+            Rotactor_Type (MMS.F_PT.F_CM.Input.Payload_Mass / 10),
+         Rotactor_2 => 
+            Rotactor_Type (MMS.F_PT.F_CM.Input.Payload_Mass mod 10)));
+   --  ??? Rotactors are computed from payload mass, which one is which?
+      
+   function CP_Displays return CP_Displays_Type is
+     (CP_Displays_Type'
+        (Ready            => MMS.F_PT.F_CM.Input.Ready_For_Takeoff,
+         Cancelled        => MMS.F_PT.F_CM.Input.Mission_Cancelled,
+         Complete         => MMS.F_PT.F_CM.Input.Mission_Complete,
+         Aborted          => MMS.F_PT.F_CM.Input.Mission_Aborted,
+         Primary_Source   => MMS.F_PT.F_CM.Input.Primary_Source,
+         Secondary_Source => MMS.F_PT.F_CM.Input.Secondary_Source));
+   
+   function Propulsion_Energy return Propulsion_Energy_Type is
+     (Propulsion_Energy_Type'
+        (Primary_Source_Capacity   => MMS.F_PT.F_CM.Input.Primary_Source,
+         Secondary_Source_Capacity => MMS.F_PT.F_CM.Input.Secondary_Source));
+   
+   function Mission_Cancelled return Boolean
+     renames MMS.F_PT.F_CM.Input.Mission_Cancelled;
+   
+   function Mission_Complete return Boolean
+     renames MMS.F_PT.F_CM.Input.Mission_Complete;
+   
+   function Mission_Aborted return Boolean
+   renames MMS.F_PT.F_CM.Input.Mission_Aborted;
+   
+   function Primary_Source return Source_Type
+   renames MMS.F_PT.F_CM.Input.Primary_Source;
+   
+   function Secondary_Source return Source_Type
+     renames MMS.F_PT.F_CM.Input.Secondary_Source;
+   
+   function Propulsion_Torque return Torque_Type
+     renames MMS.F_PT.F_CM.Input.Propulsion_Torque;
+   
+   function Braking_Torque return Torque_Type
+     renames MMS.F_PT.F_CM.Input.Braking_Torque;
+
+   -------------
+   -- To F_MM --
+   -------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
+     renames MMS.F_PT.F_CM.Input.Navigation_Parameters;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option
+     renames MMS.F_PT.F_CM.Input.Navigation_Mode;
+   
+   function Navigation_Option return Navigation_Option_Type_Option
+     renames MMS.F_PT.F_CM.Input.Navigation_Option;
+
+   function Go return Boolean
+     renames MMS.F_PT.F_CM.Input.Go;   
+
+   function Emergency_Landing return Boolean
+     renames MMS.F_PT.F_CM.Input.Emergency_Landing;
+
+   function On_OFF_Push_Button return Boolean
+     renames MMS.F_PT.F_CM.Input.On_OFF_Push_Button;
+
+   function Start_Push_Button return Boolean
+     renames MMS.F_PT.F_CM.Input.Start_Push_Button;
+
+   function Mode_Switch return Navigation_Mode_Type
+     renames MMS.F_PT.F_CM.Input.Mode_Switch;
+
+   function Bay_Switch return Bay_Switch_Type
+     renames MMS.F_PT.F_CM.Input.Bay_Switch;
+   
+   function USB_Key return USB_Key_Type_Option
+     renames MMS.F_PT.F_CM.Input.USB_Key; 
+
+   ----------------------
+   -- To F_MM and F_FC --
+   ----------------------
+
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.F_PT.F_CM.Input.Payload_Mass;
+   
+   -------------
+   -- To F_FC --
+   -------------
+
+   function P return Distance_Type renames MMS.F_PT.F_CM.Input.P;
+   
+   function P_Dot return Speed_Type renames MMS.F_PT.F_CM.Input.P_Dot;
+   
+   function Q return Angle_Type renames MMS.F_PT.F_CM.Input.Q;
+   
+end MMS.F_PT.F_CM.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm.ads
@@ -0,0 +1,7 @@
+with Types; use Types;
+
+package MMS.F_PT.F_CM is
+
+   
+
+end MMS.F_PT.F_CM;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-behavior.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-behavior.ads
@@ -0,0 +1,81 @@
+with MMS.F_PT.F_EM.Data;
+
+package MMS.F_PT.F_EM.Behavior with SPARK_Mode is
+      
+   ------------
+   -- Inputs --
+   ------------
+
+   function Propulsion_Torque return Torque_Type with Global => Private_State;
+   
+   function Braking_Torque return Torque_Type with Global => Private_State;
+
+   function P_Dot return Speed_Type with Global => Private_State;
+
+   ---------------------------------------
+   -- Behavioural Specification of F_EM --
+   ---------------------------------------
+
+   procedure Read_Inputs with
+   --  Read values of inputs once and for all and update the current state
+     Global => (In_Out => Private_State);
+
+   procedure Write_Outputs with
+   --  Compute values of outputs from the current state
+     Global => (Input  => Private_State,
+                Output => Output_State);
+
+   procedure Run with
+     Global => (In_Out => Private_State);
+   
+private
+   
+   function Primary_Initial_Capacity return Energy_Level_Type 
+   is
+     (Data.Primary_Initial_Capacity + Data.Secondary_Initial_CapacitY)
+   with Global => Private_State;
+      
+   function Propulsion_Energy return Energy_Level_Type
+     with Global => Private_State;
+   --  Integral [0-t] Propulsion_Torque(u) * P_Dot(u) * du
+   
+   function Braking_Energy return Energy_Level_Type
+     with Global => Private_State;
+   --  Integral [0-t] Braking_Torque(u) * P_Dot(u) * du
+   
+   function Dispended_Energy return Energy_Level_Type
+   is 
+     (Propulsion_Energy + Braking_Energy)
+   with Global => Private_State;
+   
+   function Primary_Energy_Left return Energy_Level_Type
+   is
+     (Data.Primary_Initial_Capacity - Dispended_Energy)
+   with Global => Private_State;
+   
+   function Primary_Source return Source_Type 
+   is  
+     (Source_Type (100 *
+                   (Data.Primary_Initial_Capacity - Dispended_Energy /
+                      Data.Primary_Initial_Capacity)))
+   with Global => Private_State;
+   
+   function Secondary_Energy_Left return Energy_Level_Type
+   is
+     (if Primary_Source > 0 then 
+         Data.Secondary_Initial_Capacity
+      else
+         Data.Secondary_Initial_Capacity - Dispended_Energy)
+   with Global => Private_State;
+   
+   function Secondary_Source return Source_Type 
+   is
+     (if Primary_Source > 0 then 
+         100
+      else
+         Source_Type (100 *
+                      (Data.Secondary_Initial_Capacity - Dispended_Energy /
+                         Data.Secondary_Initial_Capacity)))
+   with Global => Private_State;
+     
+end MMS.F_PT.F_EM.Behavior;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-data.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-data.ads
@@ -0,0 +1,14 @@
+with Types; use Types;
+
+package MMS.F_PT.F_EM.Data is
+
+   ---------------
+   -- Constants --
+   ---------------
+   
+   --  From 6.8.4
+   
+   Primary_Initial_Capacity   : Energy_Level_Type;
+   Secondary_Initial_Capacity : Energy_Level_Type;
+
+end MMS.F_PT.F_EM.Data;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-input.ads
@@ -0,0 +1,25 @@
+with MMS.F_PT.F_FC.Output;
+with MMS.F_PT.F_CM.Output;
+
+with Types; use Types;
+
+package MMS.F_PT.F_EM.Input is
+
+   ---------------
+   -- From F_FC --
+   ---------------
+   
+   function Propulsion_Torque return Torque_Type
+     renames MMS.F_PT.F_FC.Output.Propulsion_Torque;
+   
+   function Braking_Torque return Torque_Type
+     renames MMS.F_PT.F_FC.Output.Propulsion_Torque;
+   
+   ---------------
+   -- From F_CM --
+   ---------------
+   
+   function P_Dot return Speed_Type
+     renames MMS.F_PT.F_CM.Output.P_Dot;
+
+end MMS.F_PT.F_EM.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-output.ads
@@ -0,0 +1,19 @@
+with Types; use Types;
+
+package MMS.F_PT.F_EM.Output is
+
+   -------------
+   -- To F_CM --
+   -------------
+   
+   function Primary_Source return Source_Type with Global => Output_State;
+   
+   function Secondary_Source return Source_Type with Global => Output_State;
+   
+   -------------
+   -- To F_MM --
+   -------------
+   
+   function Energy_Level return Energy_Level_Type with Global => Output_State;
+   
+end MMS.F_PT.F_EM.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-state.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-state.ads
@@ -0,0 +1,4 @@
+private
+package MMS.F_PT.F_EM.State is
+   
+end MMS.F_PT.F_EM.State;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em.ads
@@ -0,0 +1,6 @@
+with Types; use Types;
+
+package MMS.F_PT.F_EM with Abstract_State => (Private_State, Output_State) is
+   pragma Elaborate_Body (MMS.F_PT.F_EM);
+   
+end MMS.F_PT.F_EM;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.adb
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.adb
@@ -0,0 +1,43 @@
+with MMS.F_PT.F_FC.State;
+
+package body MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
+
+   Stored_Time_Since_In_Safety_Escape : Time_Type with Ghost;
+   function Get_Time_Since_In_Safety_Escape return Time_Type is
+     (Stored_Time_Since_In_Safety_Escape);
+
+   procedure Run is
+   begin
+      if On_State = RUNNING then
+         Check_Safety_Escape;
+         if not In_Safety_Envelope then
+            Stored_Time_Since_In_Safety_Escape := Time_Since_In_Safety_Escape;
+         end if;
+
+         Choose_Operating_Mode;
+      end if;
+
+      AV_State_Vector;
+      Update_State;
+
+      if On_State = RUNNING then
+         Propulsion_Braking_Mutual_Exclusion;
+
+         Reference_Trajectory_Computation;
+
+         if Engine_State = PROPULSION then
+            Gain_Scheduling;
+            Propulsion_Control;
+            State.Braking_Torque := 0.0;
+         elsif Engine_State = BRAKING then
+            Gain_Scheduling;
+            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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.ads
@@ -0,0 +1,45 @@
+with MMS.F_PT.F_FC.Data;
+with Types; use Types;
+
+package MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   -----------------------------------
+   -- High-Level Properties on F_FC --
+   -----------------------------------
+
+   function Engine_State_In_Braking return Boolean is
+     (On_State = RUNNING
+      and then Engine_State in Braking_State_Type);
+
+   function Engine_State_In_Propulsion return Boolean is
+     (On_State = RUNNING
+      and then Engine_State in Propulsion_State_Type);
+
+   function Get_Time_Since_In_Safety_Escape return Time_Type with
+     Ghost;
+
+   -----------------------------------
+   -- High-Level Garantees for F_FC --
+   -----------------------------------
+
+   procedure Run with
+     Post =>
+
+     --  6.7.3.2.D Propulsion and braking torque actions are in mutual
+     --  exclusion.
+
+     (if (Engine_State_In_Propulsion'Old and then Engine_State_In_Braking)
+      or else (Engine_State_In_Braking'Old and then Engine_State_In_Propulsion)
+      then Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration)
+
+     --  6.7.3.2.E In-flight mission concellation with remaining propulsion
+     --  capacity implies occurrence of safety excapes for more than
+     --  Escape_Time seconds.
+
+     and then
+       (if On_State = ABORTED and then On_State'Old /= ABORTED
+           and then Aborted_With_Propulsion_Available
+        then Get_Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time);
+
+end MMS.F_PT.F_FC.Behavior.Guarantees;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior.ads
@@ -0,0 +1,793 @@
+with MMS.F_PT.F_FC.Data;
+with External;
+with Types; use Types; use all type Types.Mks.Mks_Type;
+with MMS.F_PT.Data;
+
+package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   ------------
+   -- Inputs --
+   ------------
+
+   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 => (Input => Input_State, Proof_In => Private_State),
+     Pre    => On_State = INIT;
+
+   function Start_Landing return Boolean with
+     Global => (Input => Input_State, Proof_In => Private_State),
+     Pre    => On_State = RUNNING;
+
+   function Operating_Point return Operating_Point_Type with
+     Global => Input_State;
+
+   function Operating_Mode return Navigation_Option_Type with
+     Global => Input_State;
+
+   function Mission_Range return Current_Range_Type with
+     Global => Input_State;
+
+   function Emergency_Landing return Boolean with
+     Global => Input_State;
+
+   function Payload_Mass return Payload_Mass_Type with
+     Global => Input_State;
+
+   --------------------------
+   -- Properties on Inputs --
+   --------------------------
+
+   function Operating_Point_Changed return Boolean with
+     Global => Input_State;
+
+   function Operating_Mode_Changed return Boolean with
+     Global => Input_State;
+
+   ----------------------
+   -- Estimated Values --
+   ----------------------
+
+   function Q_Dot return Speed_Type with Global => Input_State;
+
+   ------------
+   -- States --
+   ------------
+
+   function On_State return On_State_Type with
+     Global => Private_State;
+
+   function Running_State return Running_State_Type with
+     Global => Private_State;
+
+   function Engine_State return Engine_State_Type with
+     Global => (Input => Mutual_Exclusion_State, Proof_In => Private_State),
+     Pre    => On_State = RUNNING;
+
+   function Aborted_With_Propulsion_Available return Boolean with
+     Global => Private_State,
+     Pre    => On_State = ABORTED;
+
+   ----------------
+   -- Properties --
+   ----------------
+
+   --  From 6.7.3.2
+
+   function Flight_Phase return Flight_Phase_Type with
+     Global => (Input => Trajectory_State, Proof_In => Private_State),
+     Pre    => On_State = RUNNING;
+
+   function In_Safety_Envelope return Boolean 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,
+         when CRUISE  =>
+            Q_Dot in MMS.F_PT.F_FC.Data.Qdot_MinCr .. MMS.F_PT.F_FC.Data.Qdot_MaxCr
+              and Q > MMS.F_PT.F_FC.Data.Q_MinCr
+              and P_Dot < MMS.F_PT.F_FC.Data.Pdot_MaxCr,
+         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 => On_State = RUNNING;
+
+   function Selected_Option return Speed_Or_Altitude with
+     Global => (Input    => Operating_Mode_State,
+                Proof_In => Private_State),
+     Pre    => On_State = RUNNING;
+
+   function Already_Running return Boolean with
+     Global => Private_State,
+     Pre    => On_State = RUNNING;
+
+   function Time_Since_In_Safety_Escape return Time_Type with
+     Global => (Input    => Safety_Escape_State,
+                Proof_In => (Input_State, Trajectory_State, Private_State)),
+     Pre    => On_State = RUNNING and then not In_Safety_Envelope;
+
+   function Fast_Evolving_Safety_Escape return Boolean with
+     Global => (Input    => Private_State,
+                Proof_In => (Input_State, Trajectory_State)),
+     Pre    => On_State = RUNNING and then not In_Safety_Envelope;
+
+   function Time_Since_Stopped return Time_Type with
+     Global => (Input => Mutual_Exclusion_State, Proof_In => Private_State),
+     Pre    => On_State = RUNNING;
+
+   function Propulsion_Torque return Torque_Type with
+     Global => Propulsion_State;
+
+   function Braking_Torque return Torque_Type with
+     Global => Braking_State;
+
+   function Current_Speed return Current_Speed_Type with
+     Global => AV_State_Vector_State;
+
+   function Current_Altitude return Current_Altitude_Type with
+     Global => AV_State_Vector_State;
+
+   function Current_Range return Current_Range_Type with
+     Global => AV_State_Vector_State;
+
+   function Estimated_Total_Mass return Estimated_Total_Mass_Type with
+     Global => AV_State_Vector_State;
+
+   ---------------------------------------
+   -- Behavioural Specification of F_FC --
+   ---------------------------------------
+
+   procedure Read_Inputs with
+   --  Read values of inputs once and for all and update the current state
+
+     Post   => Operating_Point_Changed =
+       (Operating_Point'Old /= Operating_Point)
+     and then Operating_Mode_Changed =
+       (Operating_Mode'Old /= Operating_Mode);
+
+   procedure Write_Outputs with
+   --  Compute values of outputs from the current state
+
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Mutual_Exclusion_State,
+                           Gain_Scheduling_State,
+                           Propulsion_State,
+                           Braking_State),
+                Output => Output_State);
+
+   -----------------------
+   -- Safety Objectives --
+   -----------------------
+   --  See 7.7.3.2.E
+
+   procedure Check_Safety_Escape with
+     Global => (Input  => (Input_State, Trajectory_State),
+                In_Out => Safety_Escape_State),
+     Pre    => On_State in RUNNING,
+     Post   =>
+
+       --  Time_Since_In_Safety_Escape is the number of seconds since the first
+       --  occurrence of safety escapes.
+
+       (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));
+
+   ---------------------------------------------
+   -- Choice of Operating Mode in Energy Mode --
+   ---------------------------------------------
+   --  See 6.7.4 (Propulsion Control)
+
+   procedure Choose_Operating_Mode with
+   --  Two systems of two equations in (pdotA, qA), (pdotS, qS) are to be solved.
+   --  First:
+   --  g/L= (pdotA) ** 2 * cos(qA)
+   --  Operating_Point.Altitude = L * (1 - cos(qA))
+   --  Second<6E>:
+   --  g/L = (pdotS) ** 2 * cos(qS)
+   --  Operating_Point.Speed = pdotS * L * sin(qS)
+   --  If pdotA < pdotS, option ALTITUDE is selected otherwise SPEED is
+   --  selected.
+
+     Global => (Input  => Input_State,
+                In_Out => Operating_Mode_State),
+     Pre    => On_State = RUNNING,
+     Post   =>
+       (if Already_Running
+        and then not Operating_Mode_Changed
+        and then not Operating_Point_Changed
+        then Selected_Option = Selected_Option'Old)
+     and then
+       (if Operating_Mode in SPEED | ALTITUDE then
+          Selected_Option = Operating_Mode);
+
+   -----------------------
+   -- AV's State Vector --
+   -----------------------
+
+   procedure AV_State_Vector with
+     Global => (Input  => Input_State,
+                In_Out => AV_State_Vector_State);
+   --  The AV's state vector is defined by:
+   --  Current_Speed = L * sin(Q) * P_Dot
+   --  Current_Altitude = L * (1 - cos(Q))
+   --  Current_Range = Integral of Current_Speed over time
+   --  Estimated_Total_Mass = M0 + Payload_Mass + Micing, where Micing is an
+   --  unknown perturbation to be estimated.
+
+   --------------------------------
+   -- Update the State Automaton --
+   --------------------------------
+   --  Same states as F_MM except On/Off is not considered here
+
+   procedure Update_State with
+     Global         => (Input  => (Input_State, Trajectory_State),
+                        In_Out => Private_State),
+     Contract_Cases =>
+       ((On_State in INIT .. RUNNING)
+        and then Emergency_Landing
+        =>
+          On_State = ABORTED
+        and then not Aborted_With_Propulsion_Available,
+
+        On_State = INIT
+        and then not Emergency_Landing
+        and then Start_Take_Off
+        =>
+          On_State = RUNNING
+        and then Running_State = TAKE_OFF,
+
+        On_State = INIT
+        and then not Emergency_Landing
+        and then not Start_Take_Off
+        =>
+          On_State = INIT,
+
+        On_State = RUNNING
+        and then not Emergency_Landing
+        and then
+          (if Running_State = LANDING then
+              not (P_Dot = Zero_Speed and then Q_Dot = Zero_Speed))
+        and then not In_Safety_Envelope
+        and then Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time
+        =>
+          On_State = ABORTED
+        and then Aborted_With_Propulsion_Available,
+
+        On_State = RUNNING
+        and then not Emergency_Landing
+        and then
+          (if Running_State = LANDING then
+              not (P_Dot = Zero_Speed and then Q_Dot = Zero_Speed))
+        and then
+          (if Running_State = FLIGHT then not Start_Landing)
+        and then
+          (if Running_State = TAKE_OFF then not Operating_Point_Changed)
+        and then
+          (if not In_Safety_Envelope then
+               Time_Since_In_Safety_Escape <= MMS.F_PT.F_FC.Data.Escape_Time)
+        =>
+          On_State = RUNNING
+        and then Running_State = Running_State'Old,
+
+        On_State = RUNNING
+        and then not Emergency_Landing
+        and then Running_State = TAKE_OFF
+        and then Operating_Point_Changed
+        and then
+          (if not In_Safety_Envelope then
+               Time_Since_In_Safety_Escape <= MMS.F_PT.F_FC.Data.Escape_Time)
+        =>
+
+        --  A change in the Operating_Point means that the Take_Off phase is
+        --  over, see #28.
+
+          On_State = RUNNING
+        and then Running_State = FLIGHT,
+
+
+        On_State = RUNNING
+        and then not Emergency_Landing
+        and then Running_State = FLIGHT
+        and then Start_Landing
+        and then
+          (if not In_Safety_Envelope then
+               Time_Since_In_Safety_Escape <= MMS.F_PT.F_FC.Data.Escape_Time)
+        =>
+          On_State = RUNNING
+        and then Running_State = LANDING,
+
+        On_State = RUNNING
+        and then not Emergency_Landing
+        and then Running_State = LANDING
+        and then P_Dot = Zero_Speed and then Q_Dot = Zero_Speed
+        =>
+          On_State = COMPLETE,
+
+        (On_State in COMPLETE | ABORTED)
+        =>
+          On_State = On_State'Old),
+
+     Post           =>
+       (if On_State = RUNNING then
+          Engine_State = Engine_State'Old  -- ??? Needed due to current limitation in proof tool
+        and then Already_Running = (On_State'Old = RUNNING));
+
+   -------------------------------------------
+   -- Propulsion / Braking Mutual Exclusion --
+   -------------------------------------------
+
+   subtype Propulsion_State_Type is Engine_State_Type
+   range PROPULSION .. WAITING_BRAK;
+
+   subtype Braking_State_Type is Engine_State_Type
+   range BRAKING .. WAITING_PROP;
+
+   function Go_To_Braking return Boolean is
+     (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))
+   with
+     Pre    => On_State = RUNNING;
+
+   function Go_To_Propulsion return Boolean is
+     (In_Safety_Envelope)
+   with
+     Pre    => On_State = RUNNING;
+
+   procedure Propulsion_Braking_Mutual_Exclusion with
+     Global => (Input  => (Input_State, Trajectory_State, Private_State),
+                In_Out => Mutual_Exclusion_State),
+     Pre    => On_State = RUNNING,
+     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),
+
+        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));
+
+   --------------------------------------
+   -- Reference Trajectory Computation --
+   --------------------------------------
+
+   function Use_Set_Point_Altitude return Boolean is
+     (Running_State = LANDING or else Selected_Option = ALTITUDE)
+   with Pre => On_State = RUNNING;
+
+   function Set_Point_Altitude return Current_Altitude_Type with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+
+   function Intermediate_Set_Point_Altitude return Current_Altitude_Type with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+
+   function Close_To_Set_Point_Altitude return Boolean with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+   --  True if we are close enough to the set point. Used to avoid Zeno effect.
+
+   function Intermediate_Set_Point_Altitude_Reached return Boolean with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Already_Running
+     and then not Operating_Mode_Changed
+     and then not Operating_Point_Changed
+     and then Use_Set_Point_Altitude;
+   --  True if we have reached the previous intermediate set point.
+
+   function Use_Set_Point_Speed return Boolean is
+     (Running_State = LANDING or else Selected_Option = SPEED)
+   with Pre => On_State = RUNNING;
+
+   function Set_Point_Speed return Current_Speed_Type with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
+
+   function Intermediate_Set_Point_Speed return Current_Speed_Type with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
+
+   function Close_To_Set_Point_Speed return Boolean with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
+   --  True if we are close enough to the set point. Used to avoid Zeno effect.
+
+   function Intermediate_Set_Point_Speed_Reached return Boolean with
+     Global => (Input    => Trajectory_State,
+                Proof_In => (Input_State,
+                             Private_State,
+                             Operating_Mode_State,
+                             Mutual_Exclusion_State)),
+     Pre    => On_State = RUNNING
+     and then Already_Running
+     and then not Operating_Mode_Changed
+     and then not Operating_Point_Changed
+     and then Use_Set_Point_Speed;
+   --  True if we have reached the previous intermediate set point.
+
+   function Set_Point_Distance return Current_Range_Type with
+     Global => (Input    => Trajectory_State,
+                Proof_In => Private_State),
+     Pre    => On_State = RUNNING and then Running_State = LANDING;
+
+   function Close_To_Set_Point return Boolean is
+     (if Selected_Option = ALTITUDE then Close_To_Set_Point_Altitude
+      else Close_To_Set_Point_Speed)
+   with Pre => On_State = RUNNING;
+
+   procedure Reference_Trajectory_Computation with
+     --  Computed at each cycle. Slower rates are possible but not too slow.
+
+     Global => (Input  => (Input_State, Private_State, Operating_Mode_State),
+                In_Out => Trajectory_State),
+     Pre    => On_State = RUNNING,
+     Post   =>
+
+   --  For landing, the target, or preset operating point, or (final) reference
+   --  value, is more complicated than for the other phases.
+   --  For all phases except landing there is only one target: either a Speed
+   --  value or an Altitude value. But for landing there are three of them:
+   --  - Current_Range ~ Mission_Range, i.e (Current_Range - Mission_Range
+   --     =< DeliveryPrecisionUpperBound).
+   --  - Current_Altitude = 0
+   --  - Current_Speed = 0
+   --  (see #29)
+
+       (if Running_State = LANDING then
+          Set_Point_Altitude = 0
+          and then Set_Point_Speed = 0
+          and then Set_Point_Distance = Mission_Range
+        else
+          (case Selected_Option is
+                 when ALTITUDE =>
+                   Set_Point_Altitude = Operating_Point.Altitude,
+                 when SPEED =>
+                   Set_Point_Speed = Operating_Point.Speed))
+
+     --  Instead of giving the true set-point to propulsion control, it gives
+     --  half of the change amplitude. When current intermediate set-point is
+     --  reached, a new one is computed (zeno like aspects to be addressed for
+     --  convergence).
+     --  Module is reset by any operating point change.
+
+     and then
+       (if Use_Set_Point_Speed then
+          Intermediate_Set_Point_Speed =
+          (if not Already_Running
+           or else Operating_Point_Changed
+           or else Operating_Mode_Changed
+           or else (Intermediate_Set_Point_Speed_Reached
+                    and then not Close_To_Set_Point_Speed)
+           then
+             (Set_Point_Speed + Current_Speed) / 2
+           elsif Close_To_Set_Point_Speed then Set_Point_Speed
+           else Intermediate_Set_Point_Speed'Old))
+
+     and then
+       (if Use_Set_Point_Altitude then
+          Intermediate_Set_Point_Altitude =
+          (if not Already_Running
+           or else Operating_Point_Changed
+           or else Operating_Mode_Changed
+           or else (Intermediate_Set_Point_Altitude_Reached
+                    and then not Close_To_Set_Point_Altitude)
+           then (Set_Point_Altitude + Current_Altitude) / 2
+           elsif Close_To_Set_Point_Altitude then Set_Point_Altitude
+           else Intermediate_Set_Point_Altitude'Old))
+
+    --  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).
+
+     and then Flight_Phase =
+       (if Running_State = LANDING then
+          DESCENT
+        elsif not Already_Running
+           or else Operating_Point_Changed
+           or else not Close_To_Set_Point
+        then
+            (if (Selected_Option = ALTITUDE
+                 and then Current_Altitude < Set_Point_Altitude)
+             or else
+               (Selected_Option = SPEED
+                and then Current_Speed < Set_Point_Speed)
+             then CLIMB
+             else DESCENT)
+        else CRUISE);
+
+   ---------------------
+   -- Gain Scheduling --
+   ---------------------
+
+   function Mission_Profile return Mission_Profile_Type with
+     Global => Gain_Scheduling_State;
+
+   function Distance_With_Neighbour
+     (Neighbour : Mission_Profile_Type) return Mission_Profile_Distance_Type
+   with
+    Global => Gain_Scheduling_State;
+   --  Compute the distance between Mission_Profile and its Neighbour.
+
+   function Nearest_Neighbours return Neighbour_Mission_Profiles with
+    Global => Gain_Scheduling_State;
+
+   function Extract_Gain_Triple_For_Neighbours return Gain_Triples with
+    Global => Gain_Scheduling_State;
+
+   function Interpolated_Gain_Triple return Gain_Triple with
+    Global => Gain_Scheduling_State;
+   --  Compute the interpolation of the energy levels of the neighbours of
+   --  Mission_Profile by distance-based averaging.
+
+   procedure Gain_Scheduling with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Mutual_Exclusion_State),
+                In_Out => Gain_Scheduling_State),
+     Pre    => On_State = RUNNING
+     and then Engine_State in BRAKING | PROPULSION,
+     Post   =>
+
+   --  1. Assembling mission profile.
+
+       Mission_Profile =
+        (Mass     => Payload_Mass,
+         Altitude => Current_Altitude,
+         Speed    => Current_Speed)
+
+   --  2. Computing the nearest neighbours of Mission_Profile in
+   --  Flight_Domain_Mesh, and the distance of Mission_Profile to its nearest
+   --  neignbours.
+
+       and then
+       (for all Neighbour_Center of Nearest_Neighbours.Neighbours =>
+          Neighbour_Center.Mission_Profile.M in
+            MMS.F_PT.Data.Payload_Mass_Grid'Range
+        and then Neighbour_Center.Mission_Profile.S in
+          Data.Flight_Domain_Mesh'Range (1)
+        and then Neighbour_Center.Mission_Profile.A in
+          Data.Flight_Domain_Mesh'Range (2)
+        and then Neighbour_Center.Distance =
+          Distance_With_Neighbour
+            (Mission_Profile_Type'
+               (Mass     =>
+                   MMS.F_PT.Data.Payload_Mass_Grid
+                     (Neighbour_Center.Mission_Profile.M),
+                Altitude =>
+                  Data.Flight_Domain_Mesh
+                    (Neighbour_Center.Mission_Profile.S,
+                     Neighbour_Center.Mission_Profile.A).Altitude,
+                Speed    =>
+                  Data.Flight_Domain_Mesh
+                    (Neighbour_Center.Mission_Profile.S,
+                     Neighbour_Center.Mission_Profile.A).Speed)))
+
+   --  3. Extracting gain triples for the neighbours.
+
+   and then Extract_Gain_Triple_For_Neighbours.Size =
+       Nearest_Neighbours.Size
+   and then
+       (for all I in 1 .. Extract_Gain_Triple_For_Neighbours.Size =>
+          Extract_Gain_Triple_For_Neighbours.Neighbours (I) =
+         (case Flight_Phase is
+          when CLIMB   =>
+            (if Engine_State = PROPULSION then
+               Data.Climb_Propulsion_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Climb_Braking_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)),
+          when CRUISE  =>
+            (if Engine_State = PROPULSION then
+               Data.Cruise_Propulsion_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Cruise_Braking_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)),
+          when DESCENT =>
+            (if Engine_State = PROPULSION then
+               Data.Descent_Propulsion_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Descent_Braking_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S))))
+
+   --  4. Compute MP's gain triple by interpolation of its neighbours
+   --     Set appropriate value to Interpolated_Gain_Triple.
+          ;
+
+   ------------------------
+   -- Propulsion Control --
+   ------------------------
+
+   function Propulsion_Altitude_Error return Current_Altitude_Type'Base is
+     (Current_Altitude - Intermediate_Set_Point_Altitude)
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+
+   function Propulsion_Speed_Error return Current_Speed_Type'Base is
+     (Current_Speed - Intermediate_Set_Point_Speed)
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Speed;
+
+   function Propulsion_Error return Error_Type with
+     Global => Propulsion_State;
+   --  In Flight and maybe also Take-Off phase, should be
+   --  Propulsion_Altitude_Error if Selected_Mode is ALTITUDE and
+   --  Propulsion_Speed_Error otherwise, but I am confused about the units...
+   --  In Landing phase, should depend on speed, altitude, and also distance,
+   --  see #29.
+
+   function Propulsion_Integral_Error return Error_Type with
+     Global => Propulsion_State;
+   --  Cumulative past Propulsion_Error during the last Ti seconds
+
+   function Propulsion_Derivative_Error return Error_Type with
+     Global => Propulsion_State;
+   --  Propulsion_Error variation at current time
+
+   procedure Propulsion_Control with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Gain_Scheduling_State,
+                           Mutual_Exclusion_State),
+                In_Out => Propulsion_State),
+     Pre    => On_State = RUNNING
+     and then Engine_State = PROPULSION,
+     Post   => Propulsion_Torque =
+       Torque_Type (Interpolated_Gain_Triple.Kp * Propulsion_Error) +
+       Torque_Type (Interpolated_Gain_Triple.Ki * Propulsion_Integral_Error) +
+       Torque_Type (Interpolated_Gain_Triple.Kd * Propulsion_Derivative_Error);
+
+   ---------------------
+   -- Braking Control --
+   ---------------------
+
+   function Braking_Altitude_Error return Current_Altitude_Type'Base is
+     (Current_Altitude - Intermediate_Set_Point_Altitude)
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+
+   function Braking_Speed_Error return Current_Speed_Type'Base is
+     (Current_Speed - Intermediate_Set_Point_Speed)
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Speed;
+
+   function Braking_Error return Error_Type with
+     Global => Braking_State;
+   --  Same as propulsion, see #28.
+
+   function Braking_Integral_Error return Error_Type with
+     Global => Braking_State;
+   --  Cumulative past Braking_Error during the last Ti seconds
+
+   function Braking_Derivative_Error return Error_Type with
+     Global => Braking_State;
+   --  Braking_Error variation at current time
+
+   procedure Braking_Control with
+     Global => (Input  => (Input_State,
+                           Trajectory_State,
+                           Private_State,
+                           Gain_Scheduling_State,
+                           Mutual_Exclusion_State),
+                In_Out => Braking_State),
+     Pre    => On_State = RUNNING
+     and then Engine_State = BRAKING,
+     Post   => Braking_Torque =
+       Torque_Type (Interpolated_Gain_Triple.Kp * Braking_Error) +
+       Torque_Type (Interpolated_Gain_Triple.Ki * Braking_Integral_Error) +
+       Torque_Type (Interpolated_Gain_Triple.Kd * Braking_Derivative_Error);
+
+end MMS.F_PT.F_FC.Behavior;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-data.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-data.ads
@@ -0,0 +1,131 @@
+with MMS.F_PT.Data;
+
+with Types; use Types;
+
+package MMS.F_PT.F_FC.Data with SPARK_Mode is
+
+   --  ??? Types need to be precisely defined.
+
+   ------------
+   -- Tables --
+   ------------
+
+   --  From 6.7.2.3
+
+   Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Climb_Propulsion_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Cruise_Propulsion_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Descent_Propulsion_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Climb_Braking_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Cruise_Braking_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Descent_Braking_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   ---------------
+   -- Constants --
+   ---------------
+
+   --  From 6.7.3.2
+
+   Qdot_MinCl : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxCl : constant Speed_Type; --  in angle.s-1
+   Q_MaxCl    : constant Angle_Type; --  in angle
+   Qdot_MinCr : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxCr : constant Speed_Type; --  in angle.s-1
+   Q_MinCr    : constant Angle_Type; --  in angle
+   Pdot_MaxCr : constant Speed_Type; --  in angle.s-1
+   Qdot_MinDs : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxDs : constant Speed_Type; --  in angle.s-1
+   Q_MaxDs    : constant Angle_Type; --  in angle
+
+   Escape_Time : constant Time_Type; --  in s
+
+   --  From 6.7.4
+
+   Commutation_Duration : constant Time_Type; --  in s
+   Hazard_Duration      : constant Time_Type; --  in s
+
+   Recovery_Speed : constant Current_Speed_Type; --  in m.s
+
+   J0 : constant Integer; --  in kg.m2
+   L  : constant Integer; --  in m
+   M0 : constant Integer; --  in kg
+
+private
+   pragma SPARK_Mode (Off);
+
+   Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100) :=
+     (others => (others => <>));
+
+   Qdot_MinCl : constant Speed_Type := Zero_Speed;
+   Qdot_MaxCl : constant Speed_Type := Zero_Speed;
+   Q_MaxCl    : constant Angle_Type := 0.0;
+   Qdot_MinCr : constant Speed_Type := Zero_Speed;
+   Qdot_MaxCr : constant Speed_Type := Zero_Speed;
+   Q_MinCr    : constant Angle_Type := 0.0;
+   Pdot_MaxCr : constant Speed_Type := Zero_Speed;
+   Qdot_MinDs : constant Speed_Type := Zero_Speed;
+   Qdot_MaxDs : constant Speed_Type := Zero_Speed;
+   Q_MaxDs    : constant Angle_Type := 0.0;
+
+   Escape_Time : constant Time_Type := 0;
+
+   --  From 6.7.4
+
+   Commutation_Duration : constant Time_Type := 0;
+   Hazard_Duration      : constant Time_Type := 0;
+
+   Recovery_Speed : constant Current_Speed_Type := 0;
+
+   J0 : constant Integer := 0;
+   L  : constant Integer := 0;
+   M0 : constant Integer := 0;
+
+end MMS.F_PT.F_FC.Data;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-input.ads
@@ -0,0 +1,46 @@
+with MMS.F_PT.F_CM.Output;
+with MMS.F_PT.F_MM.Output;
+
+with Types; use Types;
+
+package MMS.F_PT.F_FC.Input is
+
+   ---------------
+   -- From F_CM --
+   ---------------
+
+   function P return Distance_Type
+     renames MMS.F_PT.F_CM.Output.P;
+   
+   function P_Dot return Speed_Type
+     renames MMS.F_PT.F_CM.Output.P_Dot;
+   
+   function Q return Angle_Type
+     renames MMS.F_PT.F_CM.Output.Q;
+   
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.F_PT.F_CM.Output.Payload_Mass;
+      
+   ---------------
+   -- From F_MM --
+   ---------------
+   
+   function Start_Take_Off return Boolean
+     renames MMS.F_PT.F_MM.Output.Start_Take_Off;
+   
+   function Start_Landing return Boolean
+     renames MMS.F_PT.F_MM.Output.Start_Landing;
+
+   function Operating_Point return Operating_Point_Type
+     renames MMS.F_PT.F_MM.Output.Operating_Point;
+   
+   function Operating_Mode return Navigation_Option_Type
+     renames MMS.F_PT.F_MM.Output.Operating_Mode;
+   
+   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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-output.ads
@@ -0,0 +1,29 @@
+with Types; use Types;
+
+package MMS.F_PT.F_FC.Output is
+
+   ---------------------
+   -- To F_CM or F_EM --
+   ---------------------
+
+   function Propulsion_Torque return Torque_Type with Global => Output_State;
+   
+   function Braking_Torque return Torque_Type with Global => Output_State;
+   
+   -------------
+   -- To F_MM --
+   -------------
+   
+   function Mission_Abort return Boolean with Global => Output_State; -- ??? not listed in F_FC outputs
+   
+   function Estimated_Total_Mass return Estimated_Total_Mass_Type with Global => Output_State;
+   
+   function Current_Range return Current_Range_Type with Global => Output_State;
+   
+   function Current_Speed return Current_Speed_Type with Global => Output_State;
+   
+   function Current_Altitude return Current_Altitude_Type with Global => Output_State;
+   
+   function Current_Flight_Phase return Flight_Phase_Type with Global => Output_State;
+   
+end MMS.F_PT.F_FC.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-state.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-state.ads
@@ -0,0 +1,8 @@
+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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads
@@ -0,0 +1,81 @@
+with Types; use Types;
+
+package MMS.F_PT.F_FC with
+  Abstract_State => (Input_State,
+                     Safety_Escape_State,
+                     Operating_Mode_State,
+                     AV_State_Vector_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
+      Speed    : Current_Speed_Type;
+      Altitude : Current_Altitude_Type;
+   end record;
+
+   type Flight_Speed_Center is new Positive;
+   type Flight_Altitude_Center is new Positive;
+
+   type Flight_Domain_Mesh_Type is array
+     (Flight_Speed_Center range <>, Flight_Altitude_Center range <>)
+     of Flight_Cell_Center_Type;
+
+   type Gain_Type is new Integer; --  ??? some bounds
+
+   type Gain_Triple is record
+      Kd : Gain_Type;
+      Kp : Gain_Type;
+      Ki : Gain_Type;
+   end record;
+
+   subtype Error_Type is Gain_Type'Base; --  ??? what is the type of a PID error?
+
+   type Time_Type is new Integer; --  in s ??? some bounds
+
+   type Engine_State_Type is
+     (PROPULSION, WAITING_BRAK, BRAKING, WAITING_PROP);
+
+   type Mission_Profile_Type is record
+      Mass     : Payload_Mass_Type;
+      Altitude : Current_Altitude_Type;
+      Speed    : Current_Speed_Type;
+   end record;
+
+   type Center_Mission_Profile_Type is record
+      M : Payload_Mass_Center;
+      A : Flight_Altitude_Center;
+      S : Flight_Speed_Center;
+   end record;
+
+   type Mission_Profile_Distance_Type is new Natural;
+
+   type Neighbour_Mission_Profile_Type is record
+      Mission_Profile : Center_Mission_Profile_Type;
+      Distance        : Mission_Profile_Distance_Type;
+   end record;
+
+   type Num_Of_Neighbours is new Positive range 1 .. 8;
+
+   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 Gain_Triple_Array_Type is array (Num_Of_Neighbours range <>)
+     of Gain_Triple;
+
+   type Gain_Triples (Size : Num_Of_Neighbours) is record
+     Neighbours : Gain_Triple_Array_Type (1 .. Size);
+   end record;
+
+end MMS.F_PT.F_FC;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.adb
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.adb
@@ -0,0 +1,70 @@
+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
+      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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.ads
@@ -0,0 +1,77 @@
+--  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;
+
+package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   -----------------------------------
+   -- High-Level Properties on F_MM --
+   -----------------------------------
+
+   function In_Take_Off_State return Boolean is
+      (Power_State = On
+       and then On_State = RUNNING
+       and then Running_State = TAKE_OFF)
+   with Global => Private_State;
+
+   function Mission_Aborted return Boolean is
+      (Power_State = On
+       and then On_State = ABORTED)
+   with Global => Private_State;
+
+   function Mission_Cancelled return Boolean is
+      (Power_State = On
+       and then On_State = INIT
+       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 --
+   -----------------------------------
+
+   procedure Run with
+     Pre  => State_Invariant,
+     Post => State_Invariant
+
+      --  6.6.3.A Viability guarantee: no take-off if energy aboard is
+      --  incompatible with mission completion.
+
+      and then
+       (if In_Take_Off_State and then not In_Take_Off_State'Old then
+          Initial_Energy_Test_Succeeded)
+
+      --  6.6.3.B Any mission cancellation is signaled to CP and GS.
+
+      and then
+       (if Mission_Aborted then Mission_Aborted_Signaled)
+      and then
+       (if Mission_Cancelled then Mission_Cancelled_Signaled)
+
+      --  6.6.3.2.A Missions cancelled for energy reasons can be proven
+      --  infeasible.
+
+      and then
+       (if Mission_Aborted and then not Mission_Aborted'Old
+          and then Aborted_For_Energy_Reasons
+        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_From_Parameters = Operating_Mode_From_USB_Key
+        and then Navigation_Parameters = Navigation_Parameters_From_USB_Key);
+
+end MMS.F_PT.F_MM.Behavior.Guarantees;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior.ads
@@ -0,0 +1,871 @@
+--  This package provides the behavioural specification of F_MM. It is
+--  expressed as a contract on a Run procedure which reprents the modifications
+--  performed on the state State of F_MM at each cycle of the functionality.
+--  We write the contract using a Contract_Cases and we use SPARK to ensure
+--  that:
+--   - Information about the current State of the module are only accessed
+--     when it makes sense (represented as preconditions over accessors).
+--   - A single behaviour is specified for each case in the specification.
+--   - There is a behaviour is specified for every case in the specification.
+
+with Types; use Types;
+with External;
+with MMS.F_PT.F_MM.Data;
+private with MMS.F_PT.F_MM.State;
+with MMS.F_PT.Data;
+
+package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   ------------
+   -- Inputs --
+   ------------
+
+   function Power_On return Boolean;
+
+   function Payload_Bay_Closed return Boolean with
+     Pre => Power_On;
+
+   function Payload_Mass_Given return Boolean with
+     Pre => Power_On;
+
+   function Payload_Mass return Payload_Mass_Type with
+     Pre => Power_On and then Payload_Mass_Given;
+
+   function Navigation_Mode_From_CP return Navigation_Mode_Type with
+     Pre => Power_On;
+
+   function Navigation_Mode_From_GS_Received return Boolean with
+     Pre => Power_On;
+
+   function Navigation_Mode_From_GS return Navigation_Mode_Type with
+     Pre => Power_On and then Navigation_Mode_From_GS_Received;
+
+   function Operating_Mode_From_USB_Key return Navigation_Option_Type with
+     Pre => Power_On and then USB_Key_Present;
+
+   function Operating_Mode_From_GS_Received return Boolean with
+     Pre => Power_On;
+
+   function Operating_Mode_From_GS return Navigation_Option_Type with
+     Pre => Power_On and then Operating_Mode_From_GS_Received;
+
+   function Navigation_Parameters_From_GS_Received return Boolean with
+     Pre => Power_On;
+
+   function Navigation_Parameters_From_GS return Navigation_Parameters_Type with
+     Pre => Power_On and then Navigation_Parameters_From_GS_Received;
+
+   function USB_Key_Present return Boolean with
+     Pre => Power_On;
+
+   function Navigation_Parameters_From_USB_Key return Navigation_Parameters_Type
+   with
+     Pre => Power_On and then USB_Key_Present;
+
+   function Mission_Abort_Received return Boolean with
+     Pre => Power_On;
+
+   function Start_Or_Go_Received return Boolean with
+     Pre => Power_On;
+
+   function Current_Range return Current_Range_Type with
+   Pre => Power_On;
+
+   function Current_Speed return Current_Speed_Type with
+   Pre => Power_On;
+
+   function Current_Altitude return Current_Altitude_Type with
+   Pre => Power_On;
+
+   function Current_Flight_Phase return Flight_Phase_Type with
+     Pre => Power_On;
+
+   function Energy_Level return Energy_Level_Type with
+     Pre => Power_On;
+
+   function Mission_Parameters_Defined return Boolean is
+     (USB_Key_Present
+      or else (Navigation_Mode_From_CP = RP
+               and then Navigation_Parameters_From_GS_Received
+               and then Operating_Mode_From_GS_Received))
+   with
+   Pre  => Power_On;
+
+   function Init_Completed return Boolean is
+     (Payload_Bay_Closed
+      and then Payload_Mass_Given
+      and then Mission_Parameters_Defined)
+   with
+   Pre => Power_On;
+
+   -----------------------------------------
+   -- States of the automaton in Figure 3 --
+   -----------------------------------------
+
+   function Power_State return Power_State_Type;
+
+   function On_State return On_State_Type with
+     Pre    => Power_State = ON;
+
+   function Running_State return Running_State_Type with
+     Pre => Power_State = ON
+     and then On_State = RUNNING;
+
+   function Init_State return Init_State_Type with
+     Pre => Power_State = ON
+     and then On_State = INIT;
+
+   function Aborted_For_Energy_Reasons return Boolean with
+     Pre    => Power_State = ON
+     and then On_State = ABORTED;
+
+   function State_Invariant return Boolean is
+     (Power_On = (Power_State = On)
+      and then (if Power_State = On and then On_State = RUNNING then
+                     Init_Completed));
+   --  Global assumptions, should be maintained by the task main loop.
+
+   -----------------------------
+   -- Properties and Entities --
+   -----------------------------
+
+   function Navigation_Mode return Navigation_Mode_Type with
+     Pre    => Power_On;
+
+   function Operating_Mode_From_Parameters return Navigation_Option_Type with
+     Pre    => Power_On
+     and then Mission_Parameters_Defined;
+
+   function Operating_Mode return Navigation_Option_Type with
+     Pre    => Power_On
+     and then Mission_Parameters_Defined;
+
+   function Navigation_Parameters return Navigation_Parameters_Type
+   with Pre => Power_On
+     and then Mission_Parameters_Defined;
+
+   function Mission_Range_From_Navigation_Parameters
+     return Current_Range_Type
+   with Global =>
+       (Input => Operating_Point_State, Proof_In => Input_State),
+     Pre => Power_On
+     and then Mission_Parameters_Defined;
+   --  Fetch distance from Navigation_Parameters and do the appropriate
+   --  conversion.
+
+   function Operating_Point_From_Navigation_Parameters
+     return Operating_Point_Type
+   with Global =>
+       (Input => Operating_Point_State, Proof_In => Input_State),
+     Pre => Power_On
+     and then Mission_Parameters_Defined;
+   --  Fetch altitude and speed from Navigation_Parameters and do the
+   --  appropriate conversions.
+
+   function Mission_Range return Current_Range_Type with
+     Pre    => Power_On
+     and then Power_State = On
+     and then On_State in INIT | RUNNING
+     and then Mission_Parameters_Defined;
+
+   function Operating_Point return Operating_Point_Type with
+     Pre    =>  Power_On
+     and then Power_State = On
+     and then On_State in INIT | RUNNING
+     and then Mission_Parameters_Defined;
+
+   function Initial_Energy_Compatible_With_Mission return Boolean
+   with
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = INIT
+     and then Init_Completed;
+
+   function In_Flight_Energy_Compatible_With_Mission return Boolean
+   with
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT
+     and then Current_Flight_Phase = CRUISE;
+
+   function Current_Altitude_Close_Enough_To_ref_TakeOff return Boolean with
+     Global => Input_State;
+   --  Return True if Current_Altitude is close enough to Altitude_ref_TakeOff
+
+   function Current_Speed_Close_Enough_To_ref_TakeOff return Boolean with
+     Global => Input_State;
+   --  Return True if Current_Altitude is close enough to Speed_ref_TakeOff
+
+   function Take_Off_Over return Boolean is
+     (if Operating_Mode = ALTITUDE then
+         Current_Altitude_Close_Enough_To_ref_TakeOff
+      else Current_Speed_Close_Enough_To_ref_TakeOff)
+   with
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = TAKE_OFF
+     and then Mission_Parameters_Defined;
+
+   function Descent_Over return Boolean with
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT
+     and then Current_Flight_Phase = DESCENT;
+
+   function Landed return Boolean is
+     (Current_Speed = 0 and Current_Altitude = 0)
+   with
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = LANDING;
+
+   function Emergency_Landing return Boolean with
+     Global => Output_State;
+
+   function Mission_Aborted_Signaled return Boolean with
+     Global => Output_State;
+
+   function Mission_Cancelled_Signaled return Boolean with
+     Global => Output_State;
+
+   ---------------------------------------
+   -- Behavioural Specification of F_MM --
+   ---------------------------------------
+
+   procedure Read_Inputs with
+   --  Read values of inputs once and for all and update the current state
+     Global => (In_Out => Input_State,
+                Input  => (External.State, Private_State)),
+     Post =>
+
+   --  Only update inputs when new values are received.
+
+     (if USB_Key_Present'Old then USB_Key_Present)
+     and then (if Navigation_Parameters_From_GS_Received'Old
+               then Navigation_Parameters_From_GS_Received)
+     and then (if Operating_Mode_From_GS_Received'Old
+               then Operating_Mode_From_GS_Received)
+
+   --  Information from CP can only be changed before take-off.
+
+     and then (if Power_State = On and then On_State = RUNNING
+               then Navigation_Mode_From_CP = Navigation_Mode_From_CP'Old
+               and then Payload_Bay_Closed = Payload_Bay_Closed'Old
+               and then Payload_Mass_Given = Payload_Mass_Given'Old
+               and then
+                 (if Payload_Mass_Given then Payload_Mass = Payload_Mass'Old)
+               and then
+                 (if USB_Key_Present then
+                      USB_Key_Present'Old
+                  and then Navigation_Parameters_From_USB_Key =
+                    Navigation_Parameters_From_USB_Key'Old
+                  and then Operating_Mode_From_USB_Key =
+                    Operating_Mode_From_USB_Key'Old));
+
+   procedure Write_Outputs with
+   --  Compute values of outputs from the current state
+     Global => (Input  => Private_State,
+                Output => Output_State),
+     Post   =>
+       (if Power_State = ON and then On_State = ABORTED then
+          Emergency_Landing
+        and then Mission_Aborted_Signaled)
+     and then
+       (if Power_State = ON
+        and then On_State = INIT
+        and then Init_State = CANCELLED
+        then Mission_Cancelled_Signaled);
+
+   -------------------
+   -- Tasks of F_MM --
+   -------------------
+
+   ------------------------------------------------------------
+   --  Management of Navigation Modes / Options / Parameters --
+   ------------------------------------------------------------
+
+   procedure Management_Of_Navigation_Modes_Options_Parameters with
+   --  Compute the value of Navigation_Mode / Options / Parameters (see 6.9.4)
+
+     Global => (Input  => (Input_State, Private_State),
+                Output => Navigation_Parameter_State),
+     Pre    => Power_On,
+     Post   => Navigation_Mode =
+
+     --  In case of conflict on the navigation mode, CP prevails over GS.
+
+     (if Navigation_Mode_From_CP = A
+      or else not Navigation_Mode_From_GS_Received
+      then Navigation_Mode_From_CP
+
+     --  If CP states the mode to RC then GS can choose the navigation mode.
+
+      else Navigation_Mode_From_GS)
+
+     and then
+         (if Mission_Parameters_Defined then
+
+            Operating_Mode_From_Parameters =
+              (if Navigation_Mode_From_CP = A
+               or else not Operating_Mode_From_GS_Received
+               then Operating_Mode_From_USB_Key
+               else Operating_Mode_From_GS)
+
+              --  During take-off, the most energy efficient mode is computed once and
+          --  for all from the viability tables.
+
+          and then Operating_Mode =
+            (if Operating_Mode_From_Parameters = ENERGY
+             and then Power_State = ON
+             and then On_State = RUNNING
+             and then Running_State = TAKE_OFF
+             then Data.Energy_Mode_ref_TakeOff
+             else Operating_Mode_From_Parameters)
+
+          and then Navigation_Parameters =
+            (if Navigation_Mode_From_CP = A
+             or else not Navigation_Parameters_From_GS_Received
+             then Navigation_Parameters_From_USB_Key
+             else Navigation_Parameters_From_GS));
+
+   ---------------------------------------
+   -- Operating Point Update Management --
+   ---------------------------------------
+
+   procedure Operating_Point_Update_Management with
+   --  Compute the value of Operating_Point and Mission_Range
+
+
+     Global => (Input  =>
+                  (Input_State, Private_State, Navigation_Parameter_State),
+                In_Out => Operating_Point_State),
+     Pre    => Power_On
+       and then Mission_Parameters_Defined
+       and then Power_State = ON
+       and then On_State in INIT | RUNNING,
+
+     Post   =>
+
+         --  F_MM ensures freeze of the operating point once landing is
+         --  activated.
+
+         (if On_State = RUNNING
+           and then Running_State = LANDING
+          then Operating_Point = Operating_Point'Old
+
+          --  Take-Off preset operating point (Altitude_ref_TakeOff and
+          --  Speed_ref_TakeOff) (see #28).
+
+          elsif On_State = RUNNING
+           and then Running_State = TAKE_OFF
+          then Operating_Point =
+              Operating_Point_Type'(Altitude => Data.Altitude_ref_TakeOff,
+                                    Speed    => Data.Speed_ref_TakeOff)
+
+          --  During flight, RP mode enables modification of the operating
+          --  point.
+
+          else Operating_Point = Operating_Point_From_Navigation_Parameters)
+
+         --  RP mode enables modification of range parameter before take-off.
+
+    and then
+       (if Navigation_Mode = RP
+           and then On_State = INIT
+        then Mission_Range = Mission_Range_From_Navigation_Parameters
+        else Mission_Range = Mission_Range'Old);
+
+   ------------------------------
+   --  Mission_Viability_Logic --
+   ------------------------------
+
+   function Mission_Profile return Mission_Profile_Type with
+     Global => Viability_Logic_State;
+
+   function Appropriate_Tabulating_Function return Viability_Domain_Mesh_Type
+   with
+     Global => Viability_Logic_State;
+
+   function Distance_With_Neighbour
+     (Neighbour : Mission_Profile_Type) return Mission_Profile_Distance_Type
+   with
+    Global => Viability_Logic_State;
+   --  Compute the distance between Mission_Profile and its Neighbour.
+
+   function Nearest_Neighbours return Neighbour_Mission_Profiles with
+    Global => Viability_Logic_State;
+
+   function Extract_Energy_Level_For_Neighbours return Energy_Levels
+   with
+    Global => Viability_Logic_State;
+
+   function Interpolated_Energy_Level return Energy_Level_Type with
+    Global => Viability_Logic_State;
+   --  Compute the interpolation of the energy levels of the neighbours of
+   --  Mission_Profile by distance-based averaging.
+
+   procedure Mission_Viability_Logic with
+     Global => (Input  =>
+                  (Input_State,
+                   Private_State,
+                   Navigation_Parameter_State,
+                   Operating_Point_State),
+                 In_Out => Viability_Logic_State),
+     Pre    => Power_State = ON,
+     Post   =>
+
+   --  1. Assembling mission profile.
+
+       Mission_Profile =
+        (Mass     => Payload_Mass,
+         Distance => Current_Range,
+         Altitude => Current_Altitude,
+         Speed    => Current_Speed)
+
+   --  2. Selecting tabulating function that corresponds to navigation mode.
+
+     and then Appropriate_Tabulating_Function =
+         (if On_State = INIT and then Navigation_Mode = A
+          then Data.Amode_Initial_Domain_Mesh
+          elsif On_State = INIT and then Navigation_Mode = RP
+          then Data.RPmode_Initial_Domain_Mesh
+          elsif Navigation_Mode = A
+          then Data.Amode_Cruise_Domain_Mesh
+          else Data.RPmode_Cruise_Domain_Mesh)
+
+   --  3. Computing the nearest neighbours of Mission_Profile in
+   --  Appropriate_Tabulating_Function, and the distance of Mission_Profile to
+   --  its nearest neignbours.
+
+       and then
+       (for all Neighbour_Center of Nearest_Neighbours.Neighbours =>
+          Neighbour_Center.Mission_Profile.M in
+            MMS.F_PT.Data.Payload_Mass_Grid'Range
+        and then Neighbour_Center.Mission_Profile.D in
+          Appropriate_Tabulating_Function'Range (1)
+        and then Neighbour_Center.Mission_Profile.A in
+          Appropriate_Tabulating_Function'Range (2)
+        and then Neighbour_Center.Mission_Profile.S in
+          Appropriate_Tabulating_Function'Range (3)
+        and then Neighbour_Center.Distance =
+          Distance_With_Neighbour
+            (Mission_Profile_Type'
+               (Mass     =>
+                   MMS.F_PT.Data.Payload_Mass_Grid
+                     (Neighbour_Center.Mission_Profile.M),
+                Distance =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Distance,
+                Altitude =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Altitude,
+                Speed    =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Speed)))
+
+   --  4. Extracting energy level for the neighbours.
+
+   and then Extract_Energy_Level_For_Neighbours.Size =
+       Nearest_Neighbours.Size
+   and then
+       (for all I in 1 .. Extract_Energy_Level_For_Neighbours.Size =>
+          Extract_Energy_Level_For_Neighbours.Neighbours (I) =
+         (if On_State = INIT and then Navigation_Mode = A
+          then Data.Viability_Amode_Initial
+            (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+             D => Nearest_Neighbours.Neighbours (I).Mission_Profile.D,
+             A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+          elsif On_State = INIT and then Navigation_Mode = RP
+          then Data.Viability_RPmode_Initial
+            (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+             D => Nearest_Neighbours.Neighbours (I).Mission_Profile.D,
+             A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+          elsif Navigation_Mode = A
+          then Data.Viability_Amode_Cruise
+            (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+             D => Nearest_Neighbours.Neighbours (I).Mission_Profile.D,
+             A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+          else Data.Viability_RPmode_Cruise
+            (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+             D => Nearest_Neighbours.Neighbours (I).Mission_Profile.D,
+             A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)))
+
+   --  5. Compute MP's enery level by interpolation of its neighbours
+   --     Set appropriate value to Interpolated_Energy_Level
+          ;
+
+   procedure Initial_Mission_Viability_Logic with
+   --  Compute the value of Initial_Energy_Compatible_With_Mission. It should
+   --  be computed when Init_Completed is True.
+
+     Global => (Input  =>
+                  (Input_State,
+                   Private_State,
+                   Navigation_Parameter_State,
+                   Operating_Point_State),
+                 In_Out => Viability_Logic_State),
+     Pre  => Power_On
+     and then Power_State = ON
+     and then On_State = INIT
+     and then Init_Completed,
+
+     Post => Initial_Energy_Compatible_With_Mission =
+
+   --  In A mode, use a 30% energy margin.
+
+       ((if Navigation_Mode = A then Interpolated_Energy_Level * 13 / 10
+
+   --  In RP mode, use a 10% energy margin.
+
+         else Interpolated_Energy_Level * 11 / 10) >= Energy_Level);
+
+   procedure In_Flight_Mission_Viability_Logic with
+   --  Compute the value of In_Flight_Energy_Compatible_With_Mission. It should
+   --  be repeated at a periodic rate of F_Viability.
+   --  Set In_Flight_Energy_Compatible_With_Mission to True if Energy_Level is
+   --  at least the Interpolated_Energy_Level plus an enery margin. When
+   --  EstimatedTotalMass increases, and even more so if it increases quickly,
+   --  F_MM applies greater safety margins (see #17).
+
+     Global => (Input  =>
+                  (Input_State,
+                   Private_State,
+                   Navigation_Parameter_State,
+                   Operating_Point_State),
+                 In_Out => Viability_Logic_State),
+     Pre => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT
+     and then Current_Flight_Phase = CRUISE;
+
+   ---------------------------------
+   -- Mission Termination Control --
+   ---------------------------------
+
+   function Current_Glide_Distance return Current_Range_Type with
+    Global => Mission_Termination_State;
+   --  Compute the glide distance associated with Current_Altitude using the
+   --  Glide_Distance_Domain_Mesh table and the Glide_Distance tabulated
+   --  function.
+
+   procedure Mission_Termination_Control with
+   --  Monitor Current_Range and activate landing.
+
+     Global => (Input  =>
+                  (Input_State,
+                   Private_State,
+                   Navigation_Parameter_State,
+                   Operating_Point_State),
+                 In_Out => Mission_Termination_State),
+
+     Pre  => Power_On
+     and then Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT
+     and then Current_Flight_Phase = DESCENT,
+     Post => Descent_Over =
+       (Mission_Range - Current_Range < Current_Glide_Distance);
+
+   --------------------------------
+   -- Update the State Automaton --
+   --------------------------------
+
+   procedure Update_States with
+     Global => (Input  =>
+                  (Input_State,
+                   Navigation_Parameter_State,
+                   Operating_Point_State,
+                   Viability_Logic_State,
+                   Mission_Termination_State),
+                In_Out => Private_State),
+     Pre            =>
+       (if Power_On and then Power_State = On and then On_State = RUNNING then
+          Init_Completed),
+     Contract_Cases =>
+       (not Power_On
+        =>
+          Power_State = OFF,
+
+        Power_State = OFF
+        and then Power_On
+        =>
+          Power_State = ON
+        and then On_State = INIT
+        and then Init_State = PREPARATION,
+
+        Power_State = ON
+        and then Power_On
+        and then (On_State in INIT | RUNNING)
+        and then Mission_Abort_Received
+        =>
+          Power_State = ON
+        and then On_State = ABORTED
+        and then Aborted_For_Energy_Reasons = False,
+
+        Power_State = ON
+        and then Power_On
+        and then On_State = INIT
+        and then not Mission_Abort_Received
+        and then not Init_Completed
+        =>
+          Power_State = ON
+        and then On_State = INIT
+        and then Init_State = PREPARATION,
+
+        Power_State = ON
+        and then Power_On
+        and then On_State = INIT
+        and then not Mission_Abort_Received
+        and then Init_Completed
+        and then not Start_Or_Go_Received
+        and then Initial_Energy_Compatible_With_Mission
+        =>
+          Power_State = ON
+        and then On_State = INIT
+        and then Init_State = READY,
+
+        Power_State = ON
+        and then Power_On
+        and then On_State = INIT
+        and then not Mission_Abort_Received
+        and then Init_Completed
+        and then Start_Or_Go_Received
+        and then Initial_Energy_Compatible_With_Mission
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = TAKE_OFF,
+
+        Power_State = ON
+        and then Power_On
+        and then On_State = INIT
+        and then not Mission_Abort_Received
+        and then Init_Completed
+        and then not Initial_Energy_Compatible_With_Mission
+        =>
+          Power_State = ON
+        and then On_State = INIT
+        and then Init_State = CANCELLED,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = TAKE_OFF
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then Take_Off_Over
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = FLIGHT,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = TAKE_OFF
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then not Take_Off_Over
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = TAKE_OFF,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = FLIGHT
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then Current_Flight_Phase = CRUISE
+        and then not In_Flight_Energy_Compatible_With_Mission
+        =>
+          Power_State = ON
+        and then On_State = ABORTED
+        and then Aborted_For_Energy_Reasons = True
+        and then Mission_Aborted_Signaled
+        and then Emergency_Landing,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = FLIGHT
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then Current_Flight_Phase = DESCENT
+        and then Descent_Over
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = LANDING,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = FLIGHT
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then
+          (if Current_Flight_Phase = CRUISE then
+              In_Flight_Energy_Compatible_With_Mission
+           elsif Current_Flight_Phase = DESCENT then not Descent_Over)
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = FLIGHT,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = LANDING
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then Landed
+        =>
+          Power_State = ON
+        and then On_State = COMPLETE,
+
+        Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = LANDING
+        and then Power_On
+        and then not Mission_Abort_Received
+        and then not Landed
+        =>
+          Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = LANDING,
+
+        Power_State = ON
+        and then Power_On
+        and then (On_State in COMPLETE .. ABORTED)
+        =>
+          Power_State = ON
+        and then On_State = On_State'Old);
+
+private
+
+   ----------------------------
+   --  Definitions of Inputs --
+   ----------------------------
+
+   function Power_On return Boolean is
+     (State.Input_On_OFF_Push_Button);
+
+   function Payload_Bay_Closed return Boolean is
+     (State.Input_Bay_Switch = CLOSED);
+
+   function Payload_Mass_Given return Boolean is
+     (State.Input_Payload_Mass /= 99);
+
+   function Payload_Mass return Payload_Mass_Type is
+     (State.Input_Payload_Mass);
+
+   function Navigation_Mode_From_CP return Navigation_Mode_Type is
+     (State.Input_Mode_Switch);
+
+   function Navigation_Mode_From_GS_Received return Boolean is
+     (State.Input_Navigation_Mode.Present);
+
+   function Navigation_Mode_From_GS return Navigation_Mode_Type is
+     (State.Input_Navigation_Mode.Content);
+
+   function Operating_Mode_From_USB_Key return Navigation_Option_Type is
+     (State.Input_USB_Key.Content.Navigation_Option);
+
+   function Operating_Mode_From_GS_Received return Boolean is
+     (State.Input_Navigation_Option.Present);
+
+   function Operating_Mode_From_GS return Navigation_Option_Type is
+     (State.Input_Navigation_Option.Content);
+
+   function Navigation_Parameters_From_GS_Received return Boolean is
+     (State.Input_Navigation_Parameters.Present);
+
+   function Navigation_Parameters_From_GS return Navigation_Parameters_Type is
+     (State.Input_Navigation_Parameters.Content);
+
+   function USB_Key_Present return Boolean is
+     (State.Input_USB_Key.Present);
+
+   function Navigation_Parameters_From_USB_Key return Navigation_Parameters_Type is
+     (State.Input_USB_Key.Content.Navigation_Parameters);
+
+   function Mission_Abort_Received return Boolean is
+     (State.Input_Mission_Abort);
+
+   function Start_Or_Go_Received return Boolean is
+     (State.Input_Go or State.Input_Start_Push_Button);
+
+   function Current_Range return Current_Range_Type is
+     (State.Input_Current_Range);
+
+   function Current_Speed return Current_Speed_Type is
+     (State.Input_Current_Speed);
+
+   function Current_Altitude return Current_Altitude_Type is
+     (State.Input_Current_Altitude);
+
+   function Current_Flight_Phase return Flight_Phase_Type is
+     (State.Input_Current_Flight_Phase);
+
+   function Energy_Level return Energy_Level_Type is
+     (State.Input_Energy_Level);
+
+   ------------------------------------
+   --  Definitions of Internal State --
+   ------------------------------------
+
+   function Power_State return Power_State_Type is
+     (State.Power_State);
+
+   function On_State return On_State_Type is
+     (State.On_State);
+
+   function Running_State return Running_State_Type is
+     (State.Running_State);
+
+   function Init_State return Init_State_Type is
+     (State.Init_State);
+
+   function Aborted_For_Energy_Reasons return Boolean is
+     (State.Aborted_For_Energy_Reasons);
+
+   function Descent_Over return Boolean is
+     (State.Descent_Over);
+
+   function Navigation_Parameters return Navigation_Parameters_Type is
+     (State.Navigation_Parameters);
+
+   function Navigation_Mode return Navigation_Mode_Type is
+     (State.Navigation_Mode);
+
+   function Operating_Mode_From_Parameters return Navigation_Option_Type is
+     (State.Operating_Mode_From_Parameters);
+
+   function Operating_Mode return Navigation_Option_Type is
+     (State.Operating_Mode);
+
+   function Initial_Energy_Compatible_With_Mission return Boolean is
+     (State.Initial_Energy_Compatible_With_Mission);
+
+   function In_Flight_Energy_Compatible_With_Mission return Boolean is
+     (State.In_Flight_Energy_Compatible_With_Mission);
+
+   function Mission_Range return Current_Range_Type is
+     (State.Mission_Range);
+
+   function Operating_Point return Operating_Point_Type  is
+     (State.Operating_Point);
+
+end MMS.F_PT.F_MM.Behavior;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-data.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-data.ads
@@ -0,0 +1,79 @@
+with MMS.F_PT.Data;
+
+with Types; use Types;
+
+package MMS.F_PT.F_MM.Data is
+
+   --------------------------
+   -- Parameter Data Items --
+   --------------------------
+
+   --  From 6.6.2.3
+
+   Amode_Initial_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_Amode_Initial
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre => M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in Amode_Initial_Domain_Mesh'Range (1)
+     and then A in Amode_Initial_Domain_Mesh'Range (2)
+     and then S in Amode_Initial_Domain_Mesh'Range (3);
+
+   Amode_Cruise_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_Amode_Cruise
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in Amode_Cruise_Domain_Mesh'Range (1)
+     and then A in Amode_Cruise_Domain_Mesh'Range (2)
+     and then S in Amode_Cruise_Domain_Mesh'Range (3);
+
+   RPmode_Initial_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_RPmode_Initial
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in RPmode_Initial_Domain_Mesh'Range (1)
+     and then A in RPmode_Initial_Domain_Mesh'Range (2)
+     and then S in RPmode_Initial_Domain_Mesh'Range (3);
+
+   RPmode_Cruise_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_RPmode_Cruise
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in RPmode_Cruise_Domain_Mesh'Range (1)
+     and then A in RPmode_Cruise_Domain_Mesh'Range (2)
+     and then S in RPmode_Cruise_Domain_Mesh'Range (3);
+
+   --  From 6.6.4 Mission termination control
+
+   Glide_Distance_Domain_Mesh : Glide_Domain_Mesh_Type (1 .. 100); -- ??? bounds
+
+   function Glide_Distance
+     (AI : Glide_Altitude_Center) return Current_Range_Type
+   with Pre => AI in Glide_Distance_Domain_Mesh'Range;
+
+   --  Issue #28
+
+   Altitude_ref_TakeOff    : Current_Altitude_Type;
+   Speed_ref_TakeOff       : Current_Speed_Type;
+   Energy_Mode_ref_TakeOff : Speed_Or_Altitude;
+
+end MMS.F_PT.F_MM.Data;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-input.ads
@@ -0,0 +1,77 @@
+with MMS.F_PT.F_CM.Output;
+with MMS.F_PT.F_FC.Output;
+with MMS.F_PT.F_EM.Output;
+with MMS.F_PT.Input;
+
+with Types; use Types;
+
+package MMS.F_PT.F_MM.Input is
+   
+   ---------------
+   -- From F_CM --
+   ---------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
+     renames MMS.F_PT.F_CM.Output.Navigation_Parameters;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option
+     renames MMS.F_PT.F_CM.Output.Navigation_Mode;
+   
+   function Navigation_Option return Navigation_Option_Type_Option
+     renames MMS.F_PT.F_CM.Output.Navigation_Option;
+
+   function Go return Boolean
+     renames MMS.F_PT.F_CM.Output.Go;   
+
+   function On_OFF_Push_Button return Boolean
+     renames MMS.F_PT.F_CM.Output.On_OFF_Push_Button;
+
+   function Start_Push_Button return Boolean
+     renames MMS.F_PT.F_CM.Output.Start_Push_Button;
+
+   function Mode_Switch return Navigation_Mode_Type
+     renames MMS.F_PT.F_CM.Output.Mode_Switch;
+
+   function Bay_Switch return Bay_Switch_Type
+     renames MMS.F_PT.F_CM.Output.Bay_Switch;
+
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.F_PT.F_CM.Output.Payload_Mass;
+   
+   function USB_Key return USB_Key_Type_Option
+     renames MMS.F_PT.F_CM.Output.USB_Key;
+   
+   -----------------------
+   -- From F_FC or F_EL --
+   -----------------------
+   
+   function Mission_Abort return Boolean is
+      (MMS.F_PT.F_FC.Output.Mission_Abort or else MMS.F_PT.Input.Mission_Abort);
+   
+   ---------------
+   -- From F_FC --
+   ---------------
+   
+   function Estimated_Total_Mass return Estimated_Total_Mass_Type
+     renames MMS.F_PT.F_FC.Output.Estimated_Total_Mass;
+   
+   function Current_Range return Current_Range_Type
+     renames MMS.F_PT.F_FC.Output.Current_Range;
+   
+   function Current_Speed return Current_Speed_Type
+     renames MMS.F_PT.F_FC.Output.Current_Speed;
+   
+   function Current_Altitude return Current_Altitude_Type
+     renames MMS.F_PT.F_FC.Output.Current_Altitude;
+   
+   function Current_Flight_Phase return Flight_Phase_Type
+     renames MMS.F_PT.F_FC.Output.Current_Flight_Phase;
+   
+   ---------------
+   -- From F_EM --
+   ---------------
+   
+   function Energy_Level return Energy_Level_Type
+     renames MMS.F_PT.F_EM.Output.Energy_Level;
+   
+end MMS.F_PT.F_MM.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-output.ads
@@ -0,0 +1,38 @@
+with Types; use Types;
+
+package MMS.F_PT.F_MM.Output is
+
+   -------------
+   -- To F_CM --
+   -------------
+   
+   function Mission_Cancelled return Boolean with Global => Output_State;
+   
+   function Mission_Complete return Boolean with Global => Output_State;
+   
+   function Mission_Aborted return Boolean with Global => Output_State;
+   
+   function Ready_For_Takeoff return Boolean with Global => Output_State;
+   
+   ----------------------
+   -- To F_EL and F_CM --
+   ----------------------
+
+   function Emergency_Landing return Boolean with Global => Output_State;
+   
+   -------------
+   -- To F_FC --
+   -------------
+   
+   function Start_Take_Off return Boolean with Global => Output_State;
+   
+   function Start_Landing return Boolean with Global => Output_State;
+
+   function Operating_Point return Operating_Point_Type with Global => Output_State;
+   
+   function Operating_Mode return Navigation_Option_Type with Global => Output_State;
+   
+   function Mission_Range return Current_Range_Type with Global => Output_State;
+   -- ??? which distance type
+   
+end MMS.F_PT.F_MM.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-state.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-state.ads
@@ -0,0 +1,124 @@
+private
+package MMS.F_PT.F_MM.State is
+
+   -----------------
+   -- Input_State --
+   -----------------
+
+   Input_Navigation_Parameters : Navigation_Parameters_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Navigation_Mode : Navigation_Mode_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Navigation_Option : Navigation_Option_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Go : Boolean with Part_Of => Input_State;
+
+   Input_On_OFF_Push_Button : Boolean with Part_Of => Input_State;
+
+   Input_Start_Push_Button : Boolean with Part_Of => Input_State;
+
+   Input_Mode_Switch : Navigation_Mode_Type with Part_Of => Input_State;
+
+   Input_Bay_Switch : Bay_Switch_Type with Part_Of => Input_State;
+
+   Input_Payload_Mass : Payload_Mass_Type with Part_Of => Input_State;
+
+   Input_USB_Key : USB_Key_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Mission_Abort : Boolean with Part_Of => Input_State;
+
+   Input_Estimated_Total_Mass : Estimated_Total_Mass_Type with
+     Part_Of => Input_State;
+
+   Input_Current_Range : Current_Range_Type with Part_Of => Input_State;
+
+   Input_Current_Speed : Current_Speed_Type with Part_Of => Input_State;
+
+   Input_Current_Altitude : Current_Altitude_Type with Part_Of => Input_State;
+
+   Input_Current_Flight_Phase : Flight_Phase_Type with Part_Of => Input_State;
+
+   Input_Energy_Level : Energy_Level_Type with Part_Of => Input_State;
+
+   -------------------
+   -- Private_State --
+   -------------------
+
+   Power_State : Power_State_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_From_Parameters : Navigation_Option_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 => 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 => Operating_Point_State;
+
+   ---------------------------
+   -- Viability_Logic_State --
+   ---------------------------
+
+   Initial_Energy_Compatible_With_Mission : Boolean with
+     Part_Of => Viability_Logic_State;
+
+   In_Flight_Energy_Compatible_With_Mission : Boolean with
+     Part_Of => Viability_Logic_State;
+
+   -------------------------------
+   -- Mission_Termination_State --
+   -------------------------------
+
+   Descent_Over : Boolean with Part_Of => Mission_Termination_State;
+
+   ------------------
+   -- Output_State --
+   ------------------
+
+   Output_Mission_Cancelled : Boolean with Part_Of => Output_State;
+
+   Output_Mission_Complete : Boolean with Part_Of => Output_State;
+
+   Output_Mission_Aborted : Boolean with Part_Of => Output_State;
+
+   Output_Emergency_Landing : Boolean with Part_Of => Output_State;
+
+   Output_Start_Take_Off : Boolean with Part_Of => Output_State;
+
+   Output_Start_Landing : Boolean with Part_Of => Output_State;
+
+   Output_Operating_Point : Operating_Point_Type with Part_Of => Output_State;
+
+   Output_Operating_Mode : Navigation_Option_Type with Part_Of => Output_State;
+
+   Output_Mission_Range : Current_Range_Type with Part_Of => Output_State;
+
+end MMS.F_PT.F_MM.State;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb
@@ -0,0 +1,52 @@
+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,
+                       Input_Navigation_Mode,
+                       Input_Navigation_Option,
+                       Input_Go,
+                       Input_On_OFF_Push_Button,
+                       Input_Start_Push_Button,
+                       Input_Mode_Switch,
+                       Input_Bay_Switch,
+                       Input_Payload_Mass,
+                       Input_USB_Key,
+                       Input_Mission_Abort,
+                       Input_Estimated_Total_Mass,
+                       Input_Current_Range,
+                       Input_Current_Speed,
+                       Input_Current_Altitude,
+                       Input_Current_Flight_Phase,
+                       Input_Energy_Level),
+                    Output_State  =>
+                      (Output_Mission_Cancelled,
+                       Output_Mission_Complete,
+                       Output_Mission_Aborted,
+                       Output_Emergency_Landing,
+                       Output_Start_Take_Off,
+                       Output_Start_Landing,
+                       Output_Operating_Point,
+                       Output_Operating_Mode,
+                       Output_Mission_Range),
+                    Private_State =>
+                      (Power_State,
+                       On_State,
+                       Init_State,
+                       Running_State,
+                       Aborted_For_Energy_Reasons),
+                    Navigation_Parameter_State =>
+                      (Navigation_Mode,
+                       Operating_Mode_From_Parameters,
+                       Operating_Mode,
+                       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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads
@@ -0,0 +1,80 @@
+with Types; use Types;
+
+package MMS.F_PT.F_MM with
+  SPARK_Mode,
+  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 Init_State_Type is (PREPARATION, READY, CANCELLED);
+
+   type Viability_Cell_Center_Type is record
+      Distance     : Current_Range_Type;
+      Altitude     : Current_Altitude_Type;
+      Speed        : Current_Speed_Type;
+   end record;
+
+   type Viability_Distance_Center is new Positive;
+   type Viability_Altitude_Center is new Positive;
+   type Viability_Speed_Center is new Positive;
+
+   type Viability_Domain_Mesh_Type is array
+     (Viability_Distance_Center range <>,
+      Viability_Altitude_Center range <>,
+      Viability_Speed_Center range <>)
+     of Viability_Cell_Center_Type;
+
+   type Glide_Altitude_Center is new Positive;
+
+   type Glide_Domain_Mesh_Type is array
+     (Glide_Altitude_Center range <>) of Current_Altitude_Type;
+
+   type Mission_Profile_Type is record
+      Mass     : Payload_Mass_Type;
+      Distance : Current_Range_Type;
+      Altitude : Current_Altitude_Type;
+      Speed    : Current_Speed_Type;
+   end record;
+
+   type Center_Mission_Profile_Type is record
+      M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center;
+   end record;
+
+   type Mission_Profile_Distance_Type is new Natural;
+
+   type Neighbour_Mission_Profile_Type is record
+      Mission_Profile : Center_Mission_Profile_Type;
+      Distance        : Mission_Profile_Distance_Type;
+   end record;
+
+   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;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads
@@ -0,0 +1,61 @@
+with MMS.Input;
+with MMS.F_EL.Output;
+
+with Types; use Types;
+
+package MMS.F_PT.Input is
+
+   --------------
+   -- From MMS --
+   --------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
+     renames MMS.Input.Navigation_Parameters;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option
+     renames MMS.Input.Navigation_Mode;
+   
+   function Navigation_Option return Navigation_Option_Type_Option
+     renames MMS.Input.Navigation_Option;
+
+   function Go return Boolean
+     renames MMS.Input.Go;   
+
+   function Emergency_Landing return Boolean
+     renames MMS.Input.Emergency_Landing;
+
+   function On_OFF_Push_Button return Boolean
+     renames MMS.Input.On_OFF_Push_Button;
+
+   function Start_Push_Button return Boolean
+     renames MMS.Input.Start_Push_Button;
+
+   function Mode_Switch return Navigation_Mode_Type
+     renames MMS.Input.Mode_Switch;
+
+   function Bay_Switch return Bay_Switch_Type
+     renames MMS.Input.Bay_Switch; 
+
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.Input.Payload_Mass;
+   
+   function USB_Key return USB_Key_Type_Option
+     renames MMS.Input.USB_Key;
+   
+   function P return Distance_Type
+     renames MMS.Input.P;
+   
+   function P_Dot return Speed_Type
+     renames MMS.Input.P_Dot;
+   
+   function Q return Angle_Type
+     renames MMS.Input.Q;
+   
+   ---------------
+   -- From F_EL --
+   ---------------
+   
+   function Mission_Abort return Boolean
+     renames MMS.F_EL.Output.Mission_Abort;
+   
+end MMS.F_PT.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-output.ads
@@ -0,0 +1,49 @@
+with MMS.F_PT.F_CM.Output;
+with MMS.F_PT.F_MM.Output;
+  
+with Types; use Types;
+
+package MMS.F_PT.Output is
+   
+   -----------
+   --To MMS --
+   -----------
+
+   function CP_Switches return CP_Switches_Type 
+     renames MMS.F_PT.F_CM.Output.CP_Switches;
+   
+   function CP_Displays return CP_Displays_Type
+     renames MMS.F_PT.F_CM.Output.CP_Displays;
+   
+   function Propulsion_Energy return Propulsion_Energy_Type
+     renames MMS.F_PT.F_CM.Output.Propulsion_Energy;
+   
+   function Mission_Cancelled return Boolean
+     renames MMS.F_PT.F_CM.Output.Mission_Cancelled;
+   
+   function Mission_Complete return Boolean
+     renames MMS.F_PT.F_CM.Output.Mission_Complete;
+   
+   function Mission_Aborted return Boolean
+     renames MMS.F_PT.F_CM.Output.Mission_Aborted;
+   
+   function Primary_Source return Source_Type
+     renames MMS.F_PT.F_CM.Output.Primary_Source;
+   
+   function Secondary_Source return Source_Type
+     renames MMS.F_PT.F_CM.Output.Secondary_Source;
+   
+   function Propulsion_Torque return Torque_Type
+     renames MMS.F_PT.F_CM.Output.Propulsion_Torque;
+   
+   function Braking_Torque return Torque_Type
+     renames MMS.F_PT.F_CM.Output.Braking_Torque;
+
+   --------------
+   -- To F_EL --
+   --------------
+   
+   function Emergency_Landing return Boolean
+     renames MMS.F_PT.F_MM.Output.Emergency_Landing;
+   
+end MMS.F_PT.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt.ads
@@ -0,0 +1,33 @@
+with Types; use Types;
+
+package MMS.F_PT is
+   
+   type Current_Range_Type is range 1 .. 1_000_000; -- in meters
+   
+   type Current_Speed_Type is range 0 .. 500;  -- in km/h
+   
+   type Current_Altitude_Type is range -200 .. 1_000; -- in meters
+   
+   type Estimated_Total_Mass_Type is delta 0.1 range 5.0 .. 10.0; -- in kg ???
+   
+   type Energy_Level_Type is range 0 .. 500; -- in kj
+
+   subtype Speed_Or_Altitude is Navigation_Option_Type range SPEED .. ALTITUDE;
+   
+   type Operating_Point_Type is record
+      Altitude : Current_Altitude_Type; -- ??? which altitude type
+      Speed    : Current_Speed_Type; --  ??? which speed type
+   end record;
+
+   type Payload_Mass_Center is new Positive;
+
+   type Payload_Mass_Grid_Type is array (Payload_Mass_Center range <>)
+     of Payload_Mass_Type;
+
+   type On_State_Type is (INIT, RUNNING, COMPLETE, ABORTED);
+
+   type Running_State_Type is (TAKE_OFF, FLIGHT, LANDING);
+
+   type Flight_Phase_Type is (CLIMB, CRUISE, DESCENT);
+
+end MMS.F_PT;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-input.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-input.ads
@@ -0,0 +1,55 @@
+with Types; use Types;
+with External;
+
+package MMS.Input is
+
+   ------------------------------------------------------
+   -- Ground-based Mission Preparation and Supervision --
+   ------------------------------------------------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
+     renames External.Navigation_Parameters;
+
+   function Navigation_Mode return Navigation_Mode_Type_Option
+     renames External.Navigation_Mode;
+
+   function Navigation_Option return Navigation_Option_Type_Option
+     renames External.Navigation_Option;
+
+   function Go return Boolean renames External.Go;
+
+   function Emergency_Landing return Boolean renames External.Emergency_Landing;
+
+   --------------------------------------------------
+   -- AV-based Mission Preparation (Control Panel) --
+   --------------------------------------------------
+
+   function On_OFF_Push_Button return Boolean
+     renames External.On_OFF_Push_Button;
+
+   function Start_Push_Button return Boolean
+     renames External.Start_Push_Button;
+
+   function Mode_Switch return Navigation_Mode_Type
+     renames External.Mode_Switch;
+
+   function Bay_Switch return Bay_Switch_Type
+     renames External.Bay_Switch;
+
+   function Payload_Mass return Payload_Mass_Type
+     renames External.Payload_Mass;
+
+   function USB_Key return USB_Key_Type_Option
+     renames External.USB_Key;
+
+   -------------------------
+   -- Physical Parameters --
+   -------------------------
+
+   function P return Distance_Type renames External.P;
+
+   function P_Dot return Speed_Type renames External.P_Dot;
+
+   function Q return Angle_Type renames External.Q;
+
+end MMS.Input;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms-output.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms-output.ads
@@ -0,0 +1,47 @@
+with MMS.F_PT.Output;
+
+with Types; use Types;
+
+package MMS.Output is
+
+   -------------------------------------
+   -- Ground-based Mission Monitoring --
+   -------------------------------------
+   
+   function CP_Switches return CP_Switches_Type 
+     renames MMS.F_PT.Output.CP_Switches;
+   
+   function CP_Displays return CP_Displays_Type 
+     renames MMS.F_PT.Output.CP_Displays;
+   
+   function Propulsion_Energy return Propulsion_Energy_Type 
+     renames MMS.F_PT.Output.Propulsion_Energy;
+   
+   ----------------------------
+   -- Control Panel Displays --
+   ----------------------------
+   
+   function Mission_Cancelled return Boolean 
+     renames MMS.F_PT.Output.Mission_Cancelled;
+   
+   function Mission_Complete return Boolean 
+     renames MMS.F_PT.Output.Mission_Complete;
+   
+   function Mission_Aborted return Boolean 
+     renames MMS.F_PT.Output.Mission_Aborted;
+   
+   function Primary_Source return Source_Type 
+     renames MMS.F_PT.Output.Primary_Source;
+   
+   function Secondary_Source return Source_Type 
+     renames MMS.F_PT.Output.Secondary_Source;
+   
+   -------------------------
+   -- Physical Parameters --
+   -------------------------
+   
+   function Propulsion_Torque return Torque_Type;
+   
+   function Braking_Torque return Torque_Type;
+   
+end MMS.Output;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms.ads
@@ -0,0 +1,19 @@
+--  The structure of the MMS system has been created from the System
+--  Requirements document following the pattern below:
+--   * Components are packages.
+--   * Sub-Components are child packages.
+--   * Inputs and outputs are functions stored in child packages Comp.Input and
+--     Comp.Output.
+--   * Connections between inputs and outputs of various components are done
+--     using renamings (or eventually expression functions when necessary).
+--     Consistency of the component architecture is ensured by following the
+--     rules below:
+--      - An input package Comp.Subcomp.Input can only reference outputs of
+--        siblings Comp.*.Output or inputs of parent Comp.Input.
+--      - An output package Comp.Output can only reference its own inputs
+--        Comp.Input or outputs of its children Comp.Subcomp.Output.
+--      - In subcomponents, inputs and outputs are grouped within sections
+--        with a header specifying to which component(s) they are linked.
+
+package MMS is
+end MMS;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/mms.o
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/mms.o
--- a/UseCaseData/Layer2_MMS_SW_SPARK/types.ads
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/types.ads
@@ -0,0 +1,150 @@
+package Types with SPARK_Mode is
+
+   ----------------------------------
+   -- Types for inputs and outputs --
+   ----------------------------------
+
+   type Distance_Input_Type is range 1 .. 100; -- in n.m
+
+   type Speed_Input_Type is range 1 .. 250; -- in k.t
+
+   type Altitude_Input_Type is range -500 .. 3000; -- in ft
+
+   type Navigation_Parameters_Type is record
+      Distance : Distance_Input_Type;
+      Speed    : Speed_Input_Type;
+      Altitude : Altitude_Input_Type;
+   end record;
+
+   type Navigation_Parameters_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Parameters_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
+   type Navigation_Mode_Type is (RP, A);
+
+   type Navigation_Mode_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Mode_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
+   type Navigation_Option_Type is (SPEED, ALTITUDE, ENERGY);
+
+   type Navigation_Option_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Option_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
+   type USB_Key_Type is record
+      Navigation_Parameters : Navigation_Parameters_Type;
+      Navigation_Option     : Navigation_Option_Type;
+   end record;
+
+   type USB_Key_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : USB_Key_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
+   type Bay_Switch_Type is (OPEN, CLOSED);
+
+   type Payload_Mass_Type is new Integer range 0 .. 98; -- in kg
+
+   package Mks is
+
+      type Mks_Type is new Long_Float
+        with
+          Dimension_System => (
+           (Unit_Name => Meter,    Unit_Symbol => 'm',   Dim_Symbol => 'L'),
+           (Unit_Name => Kilogram, Unit_Symbol => "kg",  Dim_Symbol => 'M'),
+           (Unit_Name => Second,   Unit_Symbol => 's',   Dim_Symbol => 'T'),
+           (Unit_Name => Ampere,   Unit_Symbol => 'A',   Dim_Symbol => 'I'),
+           (Unit_Name => Kelvin,   Unit_Symbol => 'K',   Dim_Symbol => '@'),
+           (Unit_Name => Mole,     Unit_Symbol => "mol", Dim_Symbol => 'N'),
+           (Unit_Name => Candela,  Unit_Symbol => "cd",  Dim_Symbol => 'J'));
+
+      --  SI Base dimensioned subtypes
+
+      subtype Length is Mks_Type
+        with
+          Dimension => (Symbol => 'm',
+                        Meter  => 1,
+                        others => 0);
+
+      subtype Time is Mks_Type
+        with
+          Dimension => (Symbol => 's',
+                        Second => 1,
+                        others => 0);
+
+      subtype Speed is Mks_Type
+        with
+          Dimension => (Meter  =>  1,
+                        Second => -1,
+                        others =>  0);
+
+      subtype Angle is Mks_Type
+        with
+          Dimension => (Symbol => "rad",
+                        others => 0);
+
+      pragma Warnings (Off, "*assumed to be*");
+      m   : constant Length := 1.0;
+      s   : constant Time   := 1.0;
+      pragma Warnings (On, "*assumed to be*");
+   end Mks;
+
+   use Mks;
+
+   subtype Distance_Type is Length; -- type of P, unit and bounds ???
+
+   subtype Speed_Type is Mks.Speed; -- type of P_Dot and Q_Dot, in angle.s-1, bounds ???
+
+   Zero_Speed : constant Speed_Type := 0.0*m*s**(-1);
+
+   subtype Angle_Type is Angle; -- type of Q, unit and bounds ???
+
+   type Rotactor_Type is range 0 .. 9;
+
+   type CP_Switches_Type is record
+      Power      : Boolean;
+      Mode       : Navigation_Mode_Type;
+      Bay        : Bay_Switch_Type;
+      Start      : Boolean;
+      Rotactor_1 : Rotactor_Type;
+      Rotactor_2 : Rotactor_Type;
+   end record;
+
+   type Source_Type is range 1 .. 100;
+
+   type CP_Displays_Type is record
+      Ready            : Boolean;
+      Cancelled        : Boolean;
+      Complete         : Boolean;
+      Aborted          : Boolean; -- ???
+      Primary_Source   : Source_Type;
+      Secondary_Source : Source_Type;
+   end record;
+
+   type Propulsion_Energy_Type is record
+      Primary_Source_Capacity   : Source_Type;
+      Secondary_Source_Capacity : Source_Type;
+   end record;
+
+   type Torque_Type is delta 0.0001 range -10.0E6 .. 10.0E6; -- ???
+end Types;
--- a/UseCaseData/Layer2_MMS_SW_SPARK/types.o
+++ b/UseCaseData/Layer2_MMS_SW_SPARK/types.o