基于模型检验的路由协议验证方法研究

《基于模型检验的路由协议验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、目录第一章绪论11.1课题研究背景11.2国内外研究现状21.3论文的选题依据和内容41.4论文的结构安排5第二章模型检验及工具综述62.1模型检验概述62.1.1显式模型检验62.1.2符号模型检验82.1.3有界模型检验82.1.4抽象技术92.2模型检验工具SPIN10221建模语言Promela122.2.2性质描述■线性时序逻辑152.2.3使用SPIN验证172.3模型检验工具CBMC172.3.1CBMC建模程序内部变换特点182.3.2性质描述182.3.3使用CBMC验证192.4本章小结20第三章使用模型检验验证路由协议的方法223.1路由协议化简的基本原则223.1.1

2、路由协议简述223.1.2化简原则253.2基于模型检验的路由协议建模和验证263.3本章小结27第四章使用模型检验验证路由协议的实例分析294.1实例ZOSPF294」」OSPF基础294.1.2OSPF建模314.1.3OSPF安全性描述324.2实例之Chord334.2.1Chord基础334.2.2Chord建模354.2.3Chord正确性描述364.3实例之BGP37431BGP基础374.3.2BGP建模394.3.3BGP收敛性描述404.4本章小结41第五章实验结果与分析435.1实验结果435.1.1OSPF验证结果435」.2Chord验证结果455.1.3BGP验证

3、结果475.2SPIN与CBMC在路由协议验证上的性能对比485.3本章小结49第六章总结与展望5()6.1论文总结506.2未來工作展望50参考文献52致谢57在学期间的研究成果及发表的学术论文58图表清单图2.1基于反例的抽象精化框架10图2.2SPIN体系结构11图2.3—个Promela程序模型13图2.4—个init进程示例14图2.5—个if选择语句示例15图2.6CBMC体系结构17图2.7while循环展开的内部等价18图2.8—个CBMC模型程序file.c19图2.9file.c符号模拟执行结果示例19图2.10file.c验证结果示例之一20图2.11file.c验证结

4、果示例Z二20图4.1具有以个区域的OSPF自治系统30图4.2OSPF节点接收LSA后的处理算法31图4.3OSPF安全性质在SPIN中的LTL表示33图4.4OSPF安全性质在CBMC中的断言表示33图4.5Chord坏结构34图4.6Chord模型性质2在SPIN中的LTL表示37图4.7Chord模型性质2在CBMC中的断言表示37图5.1验证用OSPF网络43图5.2Chord模型反例145图5.3Chord模型反例245图5.4Chord模型反例346图5.5Chord模型反例446图5.6Chord实验数据对比47图5.7验证用BGP模型拓扑47表2.1基本数据类型14表2.2

5、LTL中算子的数学表达和SPIN的接收形式对照表16表2.3SPIN可验证的部分LTL公式和含义16表4.1节点N8的finger表35表4.2BGP模型收敛性表示41表5.1OSPF在SPIN上的验证数据44表5.2OSPF在CBMC上的验证数据44表5.3Chord在SPIN上的验证数据46表5.4Chord在CBMC上的验证数据47表5.5BGP在SPIN上的验证数据48注释表缩略词英文全称P2PPeertoPeerOSPFOpenShortestPathFirstRIPRoutingInformationProtocolBGPBorderGatewayProtocolAODVAdho

6、cOndemandDistanceVectorroutingOLSROptimizedLinkStateRoutingSPINSimplePromelaInterpreterBMCBoundedModelCheckingCBMCBoundedModelCheckingforC/C++HOLHigherOrderLogicLTLLinearTemporalLogicCTLComputationalTreeLogicSPFStablePathProblemBDDBinaryDecisionDiagramOBDDOrderedBinaryDecisionDiagramSATSatisfiabili

7、tySMTSatisfiabilityModuloTheoriesCEGARCounterExampleGuidedAbstractRefinementDHTDistributedHashTableQoSQualityofServiceGPSGlobalPositioningSystemLSALinkStateAdvertisementLSDBLinkStateDatabaseSPFShortestPathF