Research On PPTL Symbolic Model Checking And Its Tool Support

As an automatic program verification method, model checking technique has been applied in correctness analysis and verification of many fields such as software programs, hardware programs, communication protocols, safety protocols and so on in recent years. In model checking, a finite state transition structure model is constructed to describe the system to be verified, while a temporal logic formula is applied to formalize the expected property, then model checking algorithms are used to check whether the system to be verified satisfies the expected property or not. For well-studied temporal logics such as Linear temporal logic(LTL) and Computational tree logic(CTL), it is difficult or even impossible to express interval involved properties and cyclical properties of parallel systems. Propositional projection temporal logic(PPTL) introduces chop and projection temporal operators and is able to express the properties mentioned above. Further, it is proved that PPTL achieves full regular expressiveness and is very powerful.However, with the rapid development of software industry, programs are more and more complicated and the size of software is increasing. Model checking technique faces quite severe state space explosion problem. Symbolic model checking(SMC), based on reduced ordered binary decision diagram, is a very useful technique to fight state space explosion problem. In symbolic model checking, boolean function is used to symbolically encode states and transition relations in the system to be verified, and reduced ordered binary decision diagram is applied to complement boolean function and operations based on boolean function. In this way, the state space can be compressed and model checking technique can deal with more complicated systems and to some extent settle the state space explosion problem. Nu SMV is a model checker widely applied in both academic society and industry. In Nu SMV, specific input language is used to describe the system model, and LTL or CTL to express the expected property. Therefore, Nu SMV can handle symbolic model checking and bounded model checking based on LTL or CTL.In this paper, we propose a PPTL symbolic model checking method based on Nu SMV. In this method, the system to be verified is designed as a finite state transition automaton-Kripke structure model M,while the expected property is expressed with a PPTL formula j. First of all, the negation of the expected property ?j is transformed into its corresponding LNFG, and the transform procedure is continued to obtain the corresponding Büchi automaton model B based on the LNFG. After that, we make the set of initial states in M extend along the paths of the Büchi automaton B. When one accept state in B is infinitely often extended to and its corresponding set of system state stays nonempty, there is at least one path in the system model that satisfies ?j, therefore M|1j. We can provide a counter-example and help system designers correct the system. Under other circumstances, we give the conclusion that M|=j, which means the expected property is valid. This method is based on the Kripke structure used in Nu SMV, and accepts PPTL as the property describing language, hence it increases property expressing ability of model checking. Moreover, we extend the set of system states along the Büchi automaton,thus once we find a counter example or the set of system states becomes empty, we can stop the search procedure immediately and achieve pruning in the recursive procedure.