ResearchBib Share Your Research, Maximize Your Social Impacts
Sign for Notice Everyday Sign up >> Login

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

Journal: International Journal of Computer Science and Mobile Computing - IJCSMC (Vol.2, No. 12)

Publication Date:

Authors : ;

Page : 26-39

Keywords : Model Checking; Safety Property; Must Work Function (MWF); Must Not Work Function (MNWF); Term Rewriting System;

Source : Downloadexternal Find it from : Google Scholarexternal


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.

Last modified: 2013-12-09 16:37:51