一种针对CP-nets并发模型的验证方法
状态爆炸问题导致CP-nets并发模型的正确性验证工作十分困难.提出基于并发属性的模型化简方法和基于功能组合的模型抽象方法对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正.一定程度上避免了状态爆炸问题并实现了模型验证.将上述方法应用于HMIPv6协议模型,验证了上述方法的有效性.
并发系统 形式化方法 模型验证 状态爆炸
孙涛 叶新铭
内蒙古大学计算机学院,内蒙古 呼和浩特 010021
国内会议
西安
中文
1-7
2013-08-23（万方平台首次上网日期，不代表论文的发表时间）