Model Checking of Safety Properties for Complex Systems Using MWF Inactivation and MNWF Activation?

One of the aims of model checking is to confirm a system’s safety properties. Safety properties state that undesirable events never occur. This paper describes a method that derives comprehensive and rigorous safety properties for model checking. In general, an undesirable event in a system is abstract, and so safety properties corresponding to undesirable events cannot be directly applied to model checking. To be applicable to model checking, safety properties must be derived by interpreting undesirable events in a system using the system specifications. In the model checking of complex systems, some safety properties may be neglected or insufficiently specified because the functions and/or conditions in the systems are complex. The proposed method adopts the concepts of “Must Work Function (MWF) Inactivation” and “Must Not Work Function (MNWF) Activation” to solve these issues. Comprehensive and rigorous safety properties for model checking are derived according to these concepts. Undesirable events are embodied by rewriting knowledge according to the term rewriting system. The effectiveness of the proposed method is evaluated by applying it to a wireless rail crossing system. The results show that the derived safety properties offer a significantly improved degree of comprehensiveness and rigor.