Towards Rigorous Construction of Safety Cases

Iuliia Prokhorova, Linas Laibinis, Elena Troubitsyna

    Research output: Book/Journal/ReportCommissioned reportProfessional


    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.

    Original languageUndefined/Unknown
    PublisherTurku Centre for Computer Science (TUCS)
    ISBN (Print)978-952-12-3064-6
    Publication statusPublished - 2014
    MoE publication typeD4 Published development or research report or study


    • safety-critical systems
    • safety requirements
    • formal modelling
    • formal verification
    • Event-B
    • safety cases

    Cite this