The Application And Implemenation Of Pptl Model Checking Tool

At present, the software industry is going forward under double pressures since more complicated functions are required while shorter development periods are given. A main target of software engineering is to ensure that one can develop a reliable system while the system complexity is increased. For this reason, formal methods, especially model checking techniques, have got broad application in software developments.This thesis presents a model checking approach for Propositional Projection Temporal Logic based on model checker SPIN. To this end, we introduce SPIN briefly, including its function, operational principle and verification procedure. Further, PPTL is briefly presented, including the syntax, semantics, normal form and labeled normal form graph of PPTL. Moreover, the principle of model checking of PPTL based on SPIN is elaborated. Since finite intervals cannot be recognised by SPIN, we solve this problem by improving the transition mechanism of NEVER CLAIM. Based on the strategy of improvement proposed, a better model checking system, PPTL-ModelChecker, is implemented. In addition, to illustrate the efficiency and practicability of PPTL-ModelChecker, four examples are modeled, model checked and analyzed. These instances are concerned with cryptographic security protocol, uncrytographic security protocol, deadlock and aliveness respectively. Finally, the merits and drawbacks of PPTL-ModelChecker are concluded.