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

摘要：

状态爆炸问题导致CP nets并发模型的正确性验证工作十分困难.提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正.这在一定程度上避免了状态爆炸问题并实现了模型验证.通过将上述方法应用于HMIPv6协议模型,验证了其有效性.

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

所属期刊栏目：41

分类号：TP301.2(计算技术、计算机技术)

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

在线出版日期：2014-09-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：135-139,161