-
题名基于抽象和组合方法的网络协议验证
- 1
-
-
作者
陈道喜
张广泉
徐成凯
陈国彬
-
机构
苏州技师学院
苏州大学计算机科学与技术学院
重庆工商大学融智学院
-
出处
《计算机科学》
CSCD
北大核心
2015年第7期118-121,共4页
-
基金
江苏省自然科学基金(BK2011281)
苏州市应用基础研究计划(SYG201241)
+1 种基金
江苏省普通高校研究生科研创新计划(CXLX13_820)
重庆市教委科学技术研究项目(KJ133103)资助
-
文摘
由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
-
关键词
KRIPKE结构
状态爆炸
组合抽象模型
LTL模型检测
-
Keywords
Kripke structure
State explosion
composition abstraction model
LTL model checking
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
