Research On Heuristic Model Checking Method For CPN Model Of Parallel Software Based On LTL

At present,parallel software systems are widely used in various fields of life.The execution process of parallel software is complex and its state space is huge,which makes it difficult to verify the correctness of parallel software.Colored Petri Net(CPN)is good at modeling parallel software systems.Testing technology of parallel software based on CPN model has advantages in generating test sequence and coverage analysis.The correctness of the model is the premise of those methods,model checking plays an important role in ensuring the correctness of the model.The traditional model checking methods of CPN rely on exhaustive search in state space.Because of the uncertainty of executing the parallel behaviors,the state space of parallel software system model is too large to generated completely,and the traditional model checking methods can not achieve ideal results.In this dissertation,a heuristic simulation checking method is proposed for the CPN model of parallel software system.In the process of simulation,heuristic methods such as path evaluation are used to verify the attribute,which can efficiently complete the model checking without pre-generating state space of model.The main contents of this dissertation are as follows:(1)The counterexample verification method for CPN model is proposed.Linear Temporal Logic is used to describe attributes of the model.In the process of simulation,the paths satisfying the negative formula are searched.(2)This dissertation proposes a simulation method for CPN model checking,which does not pre-generate the state space,completes the attribute verification in the simulation process.The simulation method mainly includes two parts: getting the enabled transitions and state deduction.(3)A heuristic model checking method is proposed.In process of simulation and validation,the subformulas satisfied by paths are labeled and the evaluation of paths is completed.According to results of evaluation,the simulation path is selected until the counterexample is found or there is no path to be simulated.This method proposed in this dissertation dynamically completes the checking for the CPN model of parallel software system via heuristic simulation,that avoids the obstacle in model checking when state explosion.The experimental results show that the heuristic method has good effect and can complete model checking efficiently.