Automated inspection method for an STAMP/STPA - Fallen Barrier Trap at Railroad Crossing -

In recent years, information systems have become large and complicated, and demand for research on accident analysis of such a system and its countermeasure construction is increasing. As an accident model based on system theory, Systems Theoretic Accident Model and Processes (STAMP) has attracted many attention. In STAMP, it is not limited to malfunctions of system components and human errors, but also has feature of possibility to analyze errors of interaction among constituent elements and interaction between constituent elements and human beings. System Theoretical Process Analysis (STPA) is a method for analyzing in advance the possibility of system accident against the interaction between the controller and the controlee. More effective accident analysis can be expected by cooperation of STAMP/SPTA and model checking based on formal method. In this paper, we describe a result of STAMP analysis example of “Fallen Barrier Trap at Railroad Crossing” with automaton model checker UPPAAL. In addition, we consider an automatic detection approach between the STAMP/STPA tool STAMP Workbench and the model checker UPPAAL.