Bridging the gap between FRAM and safety practice by applying FSM and model checking

FRAM (the functional of resonance analysis) is an accident analysis method proposed in 2004, providing a new concept for people to analyze accident. It always supports the theoretical description and analysis, however, in safety practice, some formalized models or methods are always needed to get the intuitive conclusion. The finite state machine is a kind of relatively mature formal technique, which can effectively make up for the weakness of the FRAM, realizing the formal modeling. Meanwhile, in order to achieve the automatic validation of the formal model, this paper introduced the model checker nusmv, realizing the combination of theory, technology and measure, forming a complete and feasible accident analysis method. Finally, the case of "free enterprise pioneer" capsizal accidents was analyzed in this way, the result shows that the method is feasible.