使用模型检验自动化验证路由协议

发布时间：2017-10-18 02:41

  本文关键词：使用模型检验自动化验证路由协议

  更多相关文章： 模型检验 路由协议验证 形式化方法 SPIN CBMC

【摘要】：模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例;实验二建立关注节点加入、失效和相应处理的Chord模型,寻找协议缺陷.两个模型都用显式模型检验工具SPIN和有界模型检验工具CBMC实现验证,实验结果表明SPIN解决此类问题更有优势.
【作者单位】： 南京航空航天大学计算机科学与技术学院;
【关键词】： 模型检验 路由协议验证 形式化方法 SPIN CBMC
【基金】：国家自然科学基金项目(61100034)资助 中国博士后科学基金项目(20110491411,2012T50498)资助 江苏省博士后科研计划项目(1101092C)资助
【分类号】：TP393.04
【正文快照】： 1引言模型检验是一种基于有限状态系统的形式化自动验证方法,最早由Clarke、Emerson[1]和Queille、Sifakis[2]分别独立提出.模型检验的基本思想是穷尽搜索待验证模型的有限状态空间,检验状态是否满足性质.如果存在状态不满足,生成违反性质的反例.随着模型规模的增加,并发系统

【共引文献】

中国博士学位论文全文数据库 前1条

1 江健;互联网域名系统授权机制中不一致和多重依赖问题研究[D];清华大学;2013年

【相似文献】

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

1 黄蔚;;模型检验技术的研究与应用[J];电子质量;2008年02期

2 文艳军;王戟;齐治昌;;并发反应式系统的组合模型检验与组合精化检验[J];软件学报;2007年06期

3 刘恩军;;基于线性带权值的广义表的模型检验方法[J];计算机工程与应用;2008年29期

4 董威,王戟,齐治昌;UML Statecharts的切片模型检验方法[J];电子学报;2002年S1期

5 屈婉霞;李暾;郭阳;杨晓东;;模型检验中抽象技术研究综述[J];计算机工程与应用;2006年33期

6 许翔;吴尽昭;林连南;陈剑锋;;基于交互式马尔可夫链的模型检验[J];计算机应用;2008年07期

7 屈婉霞;李暾;郭阳;杨晓东;;一种高效的显式模型检验方法[J];国防科技大学学报;2008年04期

8 谭亮;曾红卫;;反例引导的模型检验工具的设计[J];计算机工程与设计;2009年22期

9 韩葆;蔡勉;;基于模型检验的软件可信分析模型[J];计算机技术与发展;2012年10期

10 于庆梅;骆丽;;任务流模型检验的研究[J];电脑知识与技术(学术交流);2007年03期

中国重要会议论文全文数据库 前4条

1 于庆梅;骆丽;;任务流模型检验的研究[A];中国通信集成电路技术与应用研讨会文集[C];2006年

2 宗群;窦立谦;孙连坤;刘文静;;基于残差分析方法的模型检验[A];第二十七届中国控制会议论文集[C];2008年

3 曾红卫;缪淮扣;;优化基于模型检验的测试生成[A];第六届中国测试学术会议论文集[C];2010年

4 叶俊民;张振方;王敬华;李蓉;;基于模型检验技术的源程序分析研究[A];2009年全国开放式分布与并行计算机学术会议论文集(上册)[C];2009年

中国博士学位论文全文数据库 前4条

1 董威;面向UML的模型检验研究[D];中国人民解放军国防科学技术大学;2002年

2 郭建;在数字系统设计中断言验证的研究[D];西安电子科技大学;2008年

3 沈胜宇;模型检验的反例解释[D];国防科学技术大学;2005年

4 曾红卫;Web应用的验证与测试方法研究[D];上海大学;2008年

中国硕士学位论文全文数据库 前10条

1 张振方;基于模型检验的软件分析方法研究[D];华中师范大学;2009年

2 崔晓旭;商业银行评级模型检验系统的设计与实现[D];山东大学;2012年

3 陈庆锋;软件漏洞模型检验技术的研究[D];华中科技大学;2007年

4 刘霞;移动电子商务协议的模型检验分析与设计研究[D];桂林电子科技大学;2006年

5 吴宏;基于LSC的模型检验研究与实现[D];国防科学技术大学;2004年

6 顾益;结合模型检验的软件失效模式与影响分析方法研究[D];南京航空航天大学;2012年

7 刘超;基于模型检验的飞机系统安全性分析方法研究[D];南京航空航天大学;2012年

8 张曦;基于WCET分析技术的程序实时性模型检验方法研究[D];国防科学技术大学;2011年

9 韩葆;基于模型检验的软件可信性分析模型[D];北京工业大学;2012年

10 杨志;基于吴方法的高层次模型检验方法研究[D];哈尔滨工程大学;2008年

，

本文编号：1052487