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. We propose an approach to hazard analysis where system requirements are captured as monitored, controlled, mode and commanded phenomena and STPA is applied to the controlled phenomena to identify systematically the safety constraints. These are then represented formally in an Event-B specification which is amenable to formal refinement and proof.

John Colley has 20 years industrial experience in the Electronic Design Automation field, both developing and managing the development of software tools for hardware verification, spanning Verilog and VHDL simulation, code and state machine coverage and model checking. He was also responsible for the development of co-simulation interfaces to support third party logic and analog simulators, C models and hardware emulators. He has a PhD in Computer Science from the University of Southampton. He is coordinator of the FP7 ADVANCE project and leads research on combining safety analysis and formal modelling as part of ADVANCE.