Compositional Verification in the Real World of Engineering : A case study on formal requirements for a redundancy braking system at Scania CV

This master thesis studies how requirements for a safety-critical system can be formalised and their integrity verified using formal verification, especially using stochastic compositional verification. For this master thesis a redundancy braking system for an autonomous vehicle system at Scania is studied. The study presents a potential redundancy braking system with its various sub-components and their purpose. Based on EU-regulation, a scenario is presented where an autonomous vehicle is expected to brake within specific parameters to avoid collision. This scenario is used to derive formal specifications describing desired behaviour of the system's sub-components using the formalism probabilistic contract formulae. These specifications form parallel compositions describing desired behaviour for the system in order to satisfy a top-level specification. This thesis shows how stochastic compositional verification can be utilised for a safety-critical system in the automotive industry. The specifications can be used in future work to prove refinement using an algorithm for verifying refinement of parallel compositions of probabilistic contract formulae.