一种针对CP-nets并发模型的验证方法

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 abstract method based on function combination are 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 on the model to check errors, according to which errors in the original model are modified. To some extent, the state explosion problem is avoided and model validation is accomplished. By applying above-mentioned method to HMIPv6 protocol model, verify the validity of the method.