logo menu top
IET tv globe Technology - Manufacturing
Services supporting the growth of knowledge in engineering and technology image

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

John Colley

From: Safety-critical Systems Symposium, 5 - 7 February 2013, Bristol, UK

07 February 2013  Manufacturing channel

Please login to view Technology channel presentations.

About the presentation

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.

About the speaker

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.

Webcast search