基于抽象和组合方法的网络协议验证

发布时间：2017-10-09 18:35

  本文关键词：基于抽象和组合方法的网络协议验证

  更多相关文章： Kripke结构 状态爆炸 组合抽象模型 LTL模型检测

【摘要】：由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
【作者单位】： 苏州技师学院;苏州大学计算机科学与技术学院;重庆工商大学融智学院;
【关键词】： Kripke结构 状态爆炸 组合抽象模型 LTL模型检测
【基金】：江苏省自然科学基金(BK2011281) 苏州市应用基础研究计划(SYG201241) 江苏省普通高校研究生科研创新计划(CXLX13_820) 重庆市教委科学技术研究项目(KJ133103)资助
【分类号】：TP393.04;TP311.52
【正文快照】： 到稿日期:2014-06-30返修日期:2014-10-04本文受江苏省自然科学基金(BK2011281),苏州市应用基础研究计划(SYG201241),江苏省普通高校研究生科研创新计划(CXLX13_820),重庆市教委科学技术研究项目(KJ133103)资助。模型检测是一种验证有限状态并发系统的自动化技术[1]。首先要建

【参考文献】

中国期刊全文数据库 前5条

1 林惠民,张文辉;模型检测:理论、方法与应用[J];电子学报;2002年S1期

2 刘志锋;孙博;周从华;;概率实时时态认知逻辑模型检测中抽象技术的研究[J];电子学报;2013年07期

3 吕威;黄志球;陈哲;阚双龙;魏欧;;ESpin:基于SPIN的Eclipse模型检测环境[J];计算机工程与应用;2013年07期

4 曾红卫;缪淮扣;;构件组合的抽象精化验证[J];软件学报;2008年05期

5 高建华;蒋颖;;基于余归纳的最小Kripke结构的求解[J];软件学报;2014年01期

【共引文献】

中国期刊全文数据库 前10条

1 李忠慧;张广泉;;基于UPPAAL的NS密码协议模型检测分析[J];重庆师范大学学报(自然科学版);2009年04期

2 梁陈良;聂长海;徐宝文;陈振宇;;一种基于模型检验的类测试用例生成方法[J];东南大学学报(自然科学版);2007年05期

3 张O，

本文编号：1001774