Model Checking Propositional Projection Temporal Logic With Infinite Model

At present, the software industry is going forward under double pressures for more complicated product 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 have got broad applications in software developments, especially model checking techniques.This paper presents a method for model checking Propositional Projection Temporal Logic (PPTL) formulas based on SPIN. With this method, a property of a system is specified using a PPTL formula. The PPTL formula is then transformed to an Labelled Büchi Automata (LBA); further, the system model was also represented by LBA; finally, the model checking PPTL formula is done by checking whether the product of the two LBAs is empty. In the design of model checker based on PPTL formulas, we integrate model checking PPTL formulas with model checker SPIN, which uses PPTL formulas to specify the desired properties. Then model checking PPTL formula is done within SPIN.