Realization of Combined Systemic Safety Analysis of Adverse Train Control System Using Model Checking

System theoretic process analysis (STPA) and Functional resonance analysis method are two important techniques of safety analysis in embedded systems. However, both are used for systemic hazard analysis to evaluate failure and causality of the system but often used separately. In this paper, we present an approach for integrating systemic based safety analysis techniques such as STPA and FRAM. Considering the traditional definition of safety as “a condition where nothing goes wrong”, this approach makes it possible to express and analyze both hazards from control problem and coupling connection in the system. The work presented here focuses on automatic tool support for safety analysis with safety implementation of those results. The automatic tools based safety analysis brings consistency defects, and it is time consuming to automate and validate the result effectively. So, we introduced smv model checker to realize the proposed approach. Lastly using an adverse train control system case study, we demonstrate the applicability of this research.