Research And Implementation Of PPTL Model Checking Based On Multi-strategy

With the development of computer technology,software errors have brought numerous disasters in the world.The correctness,reliability and security of software have played an important role in daily life and national defense.As a formal verification method,model checking is widely used to verify hardware and software systems,embedded systems,protocol system.However,model checking also has shortcomings.Firstly,with the increasing number of states in the model,states space explosion problem becomes more serious.Secondly,the expressiveness of temporal logic available is limited.These two points are the motivation of this paper.To overcome the above mentioned problems,this paper firstly studies the theory of Propositional Projection Temporal Logic(PPTL).Then,the paper studies the theory of model checking.Finally,the paper designs and develops multi-strategy PPTL model checker PPTLMC.This paper uses PPTL to describe the desired specification.The expressiveness of PPTL is full regular which is more powerful than Linear TL(LTL)and Computation Tree Logic(CTL).In Particular,properties relevant to intervals as well as periodically repeated ones can be naturally expressed with PPTL.The contributions of this paper are outlined as follows.1.Symbolic Model Checker for PPTL is designed and implemented.It is built upon Nu SMV.The SMV language is used to describe a system model and PPTL formulas are employed to describe the properties of the system to be verified.The algorithm firstly transforms negative PPTL formula into Büchi automaton and then coverts it to the SMV.Finally,the product system of model and Büchi automaton is computed and whether the product system is empty or not is checked.2.This paper designs and develops a multi-strategy PPTL model checker toolkit,PPTLMC,which not only includes the transformation from PPTL formulas into Normal Forms,Labeled Normal Form Graphs,Büchi Automaton and satisfiability of a PPTL formula,but also integrates Symbolic Model Checker for PPTL,Bounded Model Checker for PPTL,Partial Order Model Checker for PPTL and Petri Net Model Checker for PPTL.3.With the development of mobile Internet,the development of Web-based PPTLMC tool is meaningful.This paper designs and develops Web-based PPTLMC.4.Two examples are provided to demonstrate the correctness and availability of the model checker developed.One of them is “Ferryman Problem” and the other is “AB(Alternating Bit)Protocol”.