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

Verification Method on CP-nets Concurrent Model

作　　者：孙涛[1] 叶新铭[1] 

机构地区：[1]内蒙古大学计算机学院,呼和浩特010021

出　　处：《计算机科学》2014年第7期135-139,161,共6页Computer Science

基　　金：国家自然科学基金资助项目(61262017);国家自然科学基金资助项目(61163011);内蒙古自然科学基金资助项目(2012MS0922);内蒙古自然科学基金资助项目(2011MS0912)资助

摘　　要：状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难。提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正。这在一定程度上避免了状态爆炸问题并实现了模型验证。通过将上述方法应用于HMIPv6协议模型,验证了其有效性。It is very difficult to verify concurrency models based on CP-nets because of the state space explosion prob- lem. A model reduction method based on concurrent attributes and a model abstraction method based on function combi- nation were proposed for models. Model elements not associated with the concurrent property are removed, the abstrac- tion 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 HMIPv6 protocol model, the validity of the method was verified.

关 键 词：模型验证 化简 抽象 状态爆炸 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]