Layer2_MMS_SW_SPARK behavioural specification of F_EM

UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

@@ -43,9 +43,15 @@ ACTIVITIES:
       6.6.3.1
       A. Additional guarantee: Translated as a postcondition.
 
+    - 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)
+
   * Verifications:
     The SPARK toolset can be used to check that:
     - Ada contracts are consistent. If it is a case by case contract, SPARK can check that all cases are covered and that no two cases can apply to the same inputs. If some properties or some information can only be checked in some cases, these cases can be expressed as preconditions on property or information functions and SPARK will check that they are always used in valid context.
 
     - 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.
-     

UseCaseDevelopment/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;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-data.ads

@@ -9,6 +9,6 @@ package MMS.F_PT.F_EM.Data is
    --  From 6.8.4
    
    Primary_Initial_Capacity   : Energy_Level_Type;
-   Secondary_Initial_CapacitY : Energy_Level_Type;
+   Secondary_Initial_Capacity : Energy_Level_Type;
 
 end MMS.F_PT.F_EM.Data;

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

@@ -6,14 +6,14 @@ package MMS.F_PT.F_EM.Output is
    -- To F_CM --
    -------------
    
-   function Primary_Source return Source_Type;
+   function Primary_Source return Source_Type with Global => Output_State;
    
-   function Secondary_Source return Source_Type;
+   function Secondary_Source return Source_Type with Global => Output_State;
    
    -------------
    -- To F_MM --
    -------------
    
-   function Energy_Level return Energy_Level_Type;
+   function Energy_Level return Energy_Level_Type with Global => Output_State;
    
 end MMS.F_PT.F_EM.Output;

UseCaseDevelopment/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;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em.ads

@@ -1,7 +1,6 @@
 with Types; use Types;
 
-package MMS.F_PT.F_EM is
-
-   
+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;