Abstract: It is very difficult to verify concurrency models based on CP-nets because of the state space explosion problem．A model reduction method based on concurrent attributes and a model abstraction method based on function combination were proposed for models．Model elements not associated with the concurrent property are removed,the abstraction level of the model is upgraded,the scale of state space is significantly reduced,and behaviors associated with the concurrent property are consistent with the original model．Verification methods,such as state space analysis and model checking,are used to check errors on the model,in order to modify errors in the original model ．To some extent,the state explosion problem is avoided and model validation is accomplished．By applying above-mentioned method to HMIPv6protocol model,the validity of the method was verified．

Key words: Model verification,Reduction,Abstract,State space explosion