A Formal, Systematic Approach to STPA using Event-B Refinement and Proof

System-Theoretic Process Analysis (STPA) from Leveson is a technique for hazard analysis developed to identify more thoroughly the causal factors in complex safety-critical systems, including software design errors. Event-B is a proof-based modelling language and method that enables the development of specifications using a formal notion of refinement. The speaker proposes an approach to hazard analysis where system requirements are captured as monitored, controlled, commanded and mode phenomena, and STPA is applied to the controlled phenomena to systematically identify the safety constraints. These are then represented formally in an Event-B specification which is amenable to formal refinement and proof.