Model Checking Propositional Projection Temporal Logic Based On SPIN

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 application in software developments, especially model checking techniques.This paper presents a method for model checking Propositional Projection Temporal Logic 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 a Never Claim; further, the system model was represented by a Labelled Büchi Automata; finally, the model checking PPTL formula is done by SPIN. To this end, a translator is developed to transform a PPTL formula into Never Claim used to specify the property of a system. To do so, a formula is firstly translated into its normal form. Then, according to the normal form, a normal form graphof the formula is constructed. Further, the NFG is transformed into Never Claim. We integrate the PPTL formulas translator with model checker SPIN, which use PPTL formulas to specify the desired properties. Then model checking PPTL formula is done within SPIN. Keywords: Model Checking Temporal Logic Model Checker SPIN...