The Implementation And A Verification Instance Of Partial Order Model Checker For PPTL

With the development of computer technology, the correctness and reliability have played an important role to measure the quality of the software and hardware, especially in aerospace and military control systems. As an effective automatic verification technology, model checking is very popular in related fields. The basic idea of model checking is that, we first model the given system, then describe the property of the system with a temporal logic formula, finally check whether the system satisfies the property with some model checking algorithm. If the system does not satisfy the property and a counter example is given. Although the model checking has the advantage of automatic verification, it also has shortcoming like state space explosion problem. There are many effective methods to deal with the state space explosion problem such as partial order model checking based on partial order reduction.The partial order model checker SPIN is an open source software developed by Bell Labs. It is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. System to be verified is described in Promela, and property of the system is expressed by a LTL formula, whose negative form is converted into a Büchi automaton, then the satisfaction result is given by the verifier. However, the expression of LTL is not full regular, and some properties cannot be expressed by LTL formulas, so we need a more expressive temporal logic to describe the property of the system.The expression of PPTL is full regular, and a decision procedure for PPTL formulas has been given. Therefore the SPIN based partial order model checker for PPTL is realized, and a verification instance of this model checker is given. This thesis first studies the transformation algorithms from PPTL formulas into Büchi automata, including the transformation from PPTL formulas into Labeled Normal Form Graphs, Labeled Normal Form Graphs into Generalized Büchi Automata and Generalized Büchi Automata into Büchi Automata. Then this thesis develops the partial order model checker for PPTL by adding the transformation process from PPTL formulas into Never Claim forms to SPIN, gives the class diagram, the main functions and the flow chart of every module of the transformation process, and gives two PPTL formulas to show their Labeled Normal Form Graphs, Büchi Automata and Never Claim forms generated by the transformation process. Finally, an instance of KDC protocol based on cryptographic protocol is given. The KDC protocol is modeled by Promela, and the properties of the KDC protocol is specified by PPTL formulas, then attack paths in this protocol is finded by using the partial order model checker for PPTL.