Accident rehearsal method based on functional model checking

Many incidents show that even if no failure occur, system can go wrong because of the interaction or logical design problem and lead to undesired result. These kinds of problem are derived from system design and it is necessary to analyze their existence during the functional design phase. Accident rehearsal means the development of the operational process of a specific system from initial states to final states. Its purpose is to determine whether an unexpected state or event is reachable from one specific initial state of the system. Based on this concept, model checking technique is used because of its ability to exhaustively and automatically check whether a system model meets a given specification. To find the problems of interaction and cooperation between functions, this paper proposes a functional model checking method for the requirement of complex system accident rehearsal after functional logic design. Time automata are used to system functional modeling and safety requirement is treated as property need to satisfy. With model checking tool UPPAAL, final results about whether these properties are satisfied are given and counterexamples can be gained to guide the finding of potential accident process and design improvement. At last, it illuminates how to apply this method to accident rehearsal with an actual escalator accident.