Towards Rigorous Construction of Safety Cases

Certification of safety-critical software systems requires submission of safety assurance documents, e.g., in the form of safety cases. A safety case is a justification argument used to show that a system is safe for a particular application in a particular environment. Different argumentation strategies are applied to determine the evidence for a safety case. They allow us to support a safety case with such evidence as results of hazard analysis, testing, simulation, etc. On the other hand, application of formal methods for development and verification of critical software systems is highly recommended for their certification. In this paper, we propose a methodology that combines these two activities. Firstly, it allows us to map the given system safety requirements into elements of the formal model to be constructed, which is then used for verification of these requirements. Secondly, it guides the construction of a safety case demonstrating that the safety requirements are indeed met. Consequently, the argumentation used in such a safety case allows us to support the safety case with formal proofs and model checking results as the safety evidence. Moreover, we propose a set of argument patterns that aim at facilitating the construction of (a part of) a safety case from a formal model. In this work, we utilise the Event-B formalism due to its scalability and mature tool support. We illustrate the proposed methodology by numerous small examples as well as validate it by a larger case study – a steam boiler control system.