System States Transition Safety Analysis Method Based on FSM and NuSMV

Abstract

In recent years, software safety has been a problem for safety-critical systems. Software requires multiple states to describe the behavior of system. The state transition condition control the control signals that determine the state of a system. The control signal must be able to interface reasonably and can not be contradictory and the output state, output time and timing of control signals can not be wrong in the process of system state transition. However, in the process of developing system, there may be some errors with control signals in the convergence between the state, output status, output time and output timing and it will cause the system abnormally. In response to this problem, we present a method which based on the combination of finite state machine (FSM) and model checking technology. First, build a FSM model. After that, transform FSM model into SMV program. At last, use NuSMV to detect dangerous control signals of SMV program. Results indicate that this method is able to find the software safety problem.