The Improvement And Application Of The PPTL Model Checker

As a method of formal verification, model checking has been widely developedand used in the software development process.The improvement and application of amodel checker which is based on Propositional Projection Temporal Logic(PPTL) arepresented in this thesis. This model checker is implemented by adding and modifyingsome modules of the SPIN model checker. In the PPTL model checker, the Promelalanguage is used to describe a system model and PPTL formulae are employed todescribe the properties of the system to be verified. Since PPTL formulae cannot bedirectly identified by the SPIN, so as to implement the PPTL model checker based onSPIN, they need to be converted to Never Claim which can be accepted by the SPIN.This thesis mainly studies the improved conversion algorithm which is used toconvert a PPTL formula to Never Claim. Prior to show this, this thesis presents a briefintroduction to the syntax, semantics, some equivalence relations and logic laws of thePPTL. Further we give principles and development of model checking technology, andmainly introduce some related contents of the SPIN model checker. Then, we discussthe detail translation from a PPTL formula to Never Claim: a PPTL formulaâ†'NormalForm(NF)â†'Labeled Normal Form Graph(LNFG)â†'Never Claim. And we also presentthe corresponding algorithms. The improved algorithms are exactly the generatingalgorithms of LNFG and Never Claim. Finally, to show the actual working process ofthe PPTL model checker, we describe the verification processes through two examples:the well-known German-2004cache coherence protocol and the Russian Cardsproblem.