Research And Implementation Of Multi - Valued Model Detector

Model checking is an important automatic vertification technology for system behaviors. A large number of classical model checkers are based on Boolean Logic. All behaviors of a system are described determinately. However, with the development of large and complex systems, it is necessary for the systems to proceed uncertaint or disagreement information. Classical model checkers,,such as NuSmv or Spin, can not deal with such information.Multi-valued logics support the explicit modeling of uncertainty and disagreement by allowing additional truth values in the logic. As an extension of the Boolean logic, multi-valued logics can be used for verification of these systems. So,it is urgent to develop the multi-valued model checker. This paper presents a new method of implementing multivalued model checker MVMC. The model checker MVMC works for the multi-valued logic whose truth values forms a quasi-boolean lattice. The models are described by multi-Kripke structures. The multi-valued linear-time properties to be verified include Safety property, invariant property, liveness property, persistence and dual-persistence property in multi-valued logic system.Campared with the existing multivaluded model checker xChex, the method implemented MVMC can reduce the number of states during the process of checking LTL property,which translates a multivalued Kripke structure into analogy Kripke structure. It can reduce the repeated state and avoid the watsted memory.In the end,this paper gives an example to test the multi-valued model checker MVMC and prove its effectiveness.