Integrated Safety Analysis Using Systems-Theoretic Process Analysis and Software Model Checking

Safety-critical systems are becoming increasingly more complex and reliant on software. The increase in complexity and software renders ensuring the safety of such systems increasingly difficult. Formal verification approaches can be used to prove the correctness of software; however, even perfectly correct software could lead to an accident. The difficulty is in defining appropriate safety requirements. STPA (Systems-Theoretic Process Analysis) is a modern safety analysis approach which aims to identify the potential hazardous causes in complex systems. Model checking is an efficient technique to verify software against its requirements. In this paper, we propose an approach that integrates safety analysis and verification activities to demonstrate how a systematic combination between these approaches can help safety and software engineers to derive the software safety requirements and verify them to recognize software risks. We illustrate the proposed approach by the example of the adaptive cruise control system.