State Space Simplification Method For CPN Model Checking Of Concurrent Software

Concurrent software systems are widely used in various fields of the software industry.Concurrent interaction behavior makes the number of system states increase exponentially,and the software reliability is difficult to be guaranteed.Model checking technology can automatically detect satisfiability of property based on state space,so as to find system defects,but it is difficult to carry out in state explosion.Therefore,this thesis proposes a new state space generation method for Colored Petri Net(CPN)model,which can simplify the state space and improve the efficiency model detection without affecting the results of model detection.The specific work is as follows:(1)The algorithm of property formula processing is proposed to realize the extraction of property information and type marking.In this thesis,the ASK-CTL formula of branch temporal logic is used to describe system properties,and the initial state of properties and atomic propositions are automatically read;The property type is marked according to the modal operator,which is used to determine the cut-off condition of the state space generation algorithm.(2)The algorithm of property related transition processing is proposed to realize the classification of transition types.Reading the atomic proposition of the property formula,and extracting the property transition based on the operation of identification transition projection;According to the data correlation between transitions and property transitions in the model,property related or unrelated transitions can be divided,which can be used as the basis to determine the order of unrelated concurrent behaviors when the state space is generated.(3)A state space generation algorithm based on the sequence of unrelated behaviors is proposed to simplify the state space.The key operations are as follows:(1)In the current state,when there is no token competition and there is no activation of irrelevant transition binding,one irrelevant transition binding is randomly reserved and the other binding is deleted.This operation realizes the ordering of irrelevant concurrent behavior;(2)In the current state,when there is an activatable unrelated transition with token competition,the competing unrelated transition binding is retained and other binding is deleted.This operation preserves the unrelated branch behavior while the unrelated concurrent behavior is sequenced;(3)In the current state,when all the activatable transitions are related transitions,all the binding is reserved.This operation preserves all the concurrency of the related transitions;(4)According to the property type marked,the algorithm cut-off condition is determined.This operation ends the state space generation when the property formula decision condition is satisfied.The experimental results show that the algorithm can effectively reduce the size of state space and improve the effect and efficiency of model checking without affecting the results of model checking.