System safety assessment based on STPA and model checking

Due to the current pace of technological growth, the management of system safety has evolved with complex causes of accidents that are often beyond the identification of traditional safety assessment techniques. Recently, the hazard analysis tool Systems Theory Process Analysis (STPA) has emerged as an approach to improve safety of modern complex systems in concert with other hazard analysis tools. However, the effectiveness of STPA is a debatable issue in the industry and efforts towards incorporating some level of formalization in STPA steps are welcome. In this direction, this work presents a method for combining STPA and model checking, in order to provide a formal and unambiguous representation of the system under analysis and the threats identified by STPA. A practical case study of a robotic flight simulator is presented as an example of the proposed method. The results achieved with the proposed approach indicates that the merging of the two techniques improves the knowledge about the system under design and the consistence of the design changes proposed to tackle the safety constraints identified in STPA.