基于模型检验的路由协议验证方法研究
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 注释表 | 第10-11页 |
| 第一章 绪论 | 第11-16页 |
| ·课题研究背景 | 第11-12页 |
| ·国内外研究现状 | 第12-14页 |
| ·论文的选题依据和内容 | 第14-15页 |
| ·论文的结构安排 | 第15-16页 |
| 第二章 模型检验及工具综述 | 第16-32页 |
| ·模型检验概述 | 第16-20页 |
| ·显式模型检验 | 第16-18页 |
| ·符号模型检验 | 第18页 |
| ·有界模型检验 | 第18-19页 |
| ·抽象技术 | 第19-20页 |
| ·模型检验工具SPIN | 第20-27页 |
| ·建模语言Promela | 第22-25页 |
| ·性质描述-线性时序逻辑 | 第25-27页 |
| ·使用SPIN验证 | 第27页 |
| ·模型检验工具CBMC | 第27-30页 |
| ·CBMC建模程序内部变换特点 | 第28页 |
| ·性质描述 | 第28-29页 |
| ·使用CBMC验证 | 第29-30页 |
| ·本章小结 | 第30-32页 |
| 第三章 使用模型检验验证路由协议的方法 | 第32-39页 |
| ·路由协议化简的基本原则 | 第32-36页 |
| ·路由协议简述 | 第32-35页 |
| ·化简原则 | 第35-36页 |
| ·基于模型检验的路由协议建模和验证 | 第36-37页 |
| ·本章小结 | 第37-39页 |
| 第四章 使用模型检验验证路由协议的实例分析 | 第39-53页 |
| ·实例之OSPF | 第39-43页 |
| ·OSPF基础 | 第39-41页 |
| ·OSPF建模 | 第41-42页 |
| ·OSPF安全性描述 | 第42-43页 |
| ·实例之Chord | 第43-47页 |
| ·Chord基础 | 第43-45页 |
| ·Chord建模 | 第45-46页 |
| ·Chord正确性描述 | 第46-47页 |
| ·实例之BGP | 第47-51页 |
| ·BGP基础 | 第47-49页 |
| ·BGP建模 | 第49-50页 |
| ·BGP收敛性描述 | 第50-51页 |
| ·本章小结 | 第51-53页 |
| 第五章 实验结果与分析 | 第53-60页 |
| ·实验结果 | 第53-58页 |
| ·OSPF验证结果 | 第53-55页 |
| ·Chord验证结果 | 第55-57页 |
| ·BGP验证结果 | 第57-58页 |
| ·SPIN与CBMC在路由协议验证上的性能对比 | 第58-59页 |
| ·本章小结 | 第59-60页 |
| 第六章 总结与展望 | 第60-62页 |
| ·论文总结 | 第60页 |
| ·未来工作展望 | 第60-62页 |
| 参考文献 | 第62-67页 |
| 致谢 | 第67-68页 |
| 在学期间的研究成果及发表的学术论文 | 第68页 |
