RESSAC_Use_Case/UseCaseData/Layer2_MMS_SW_SPARK/DESIGN.txt

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.