基于CPN的IS-IS协议的验证
发布时间：2021-05-22 01:58
随着网络信息化的快速发展,可靠的网络协议成为保障网络稳定的重要因素。对网络协议进行验证不仅可以最大限度地检测和纠正协议开发前期的错误和缺陷,还可以对已设计的协议进行分析和验证,找出其中潜在的错误。形式化地描述和验证协议是整个协议设计与实现的基础,对协议实现的正确性、完整性和复杂度有重要的影响。形式化的建模工具CPN不但可以提高网络协议验证的自动化程度,而且有效的保证了协议自身的正确性和无歧义性。IS-IS路由协议作为当前内部网关的主流协议之一,采用分层的网络结构,稳定性好、收敛快等优点使得IS-IS路由协议在网络中得到了广泛的应用。但到现在为止还没有关于IS-IS路由协议进行验证的文献,所以本文进行了基于CPN的IS-IS路由协议验证。本文首先通过对IS-IS路由协议的仔细研究,对IS-IS路由协议层次化结构-子网相关功能和子网独立功能模块分别进行了CPN建模；然后通过CPN建模工具的模拟执行和状态空间技术从整体上对IS-IS路由协议的正确性进行了验证；最后对IS-IS路由协议的协议属性DIS选举、LSP/CSNP引发决定进程和最短路径的更新进行了性能验证,从验证结果可以看出IS-IS...
【文章来源】：内蒙古大学内蒙古自治区 211工程院校
【文章页数】：60 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
目录
图表目录
第一章 引言
1.1 研究背景及意义
1.2 研究内容和主要工作
1.3 论文结构
第二章 背景知识介绍
2.1 IS-IS协议简介
2.2 CPN简介
2.3 CPN Tools 简介
2.4 协议验证简介
2.5 本章小结
第三章 IS-IS协议的分析
3.1 IS-IS路由协议数据的类型和建模的数据类型
3.2 IS-IS 路由协议数据的结构和建模中数据包的结构
3.3 IS-IS 路由协议功能
3.3.1 子网相关功能
3.3.2 子网独立功能
3.4 本章小结
第四章 IS-IS路由协议的形式化建模
4.1 CPN模型的抽象
4.2 数据建模
4.3 CPN层次化建模
4.3.1 TOP层模型
4.3.2 子网相关功能接收子模块
4.3.3 子网独立功能的接收进程模块
4.3.4 子网独立功能的更新进程模块
4.3.5 子网独立功能的决定进程模块
4.3.6 子网独立功能的转发进程模块
4.3.7 子网相关功能的发送进程模块
4.4 本章小结
第五章 IS-IS路由协议模型验证与分析
5.1 IS-IS路由协议正确性的验证
5.2 协议属性的验证
5.2.1 DIS属性验证
5.2.2 LSP/CSNP信息引发决定进程属性验证
5.2.3 最短路径的更新属性验证
5.3 本章小结
第六章 总结和展望
6.1 总结
6.2 未来研究方向的展望
参考文献
致谢
【参考文献】：
期刊论文
[1]Sip协议的petri网建模及性能验证[J]. 杨郁州,张伟,占东生. 微计算机信息. 2010(21)
[2]基于CPN TOOLS的网络协议建模与仿真技术研究[J]. 占东生,张伟,顾明甲. 微计算机信息. 2010(13)
[3]基于层次结构的IS-IS协议一致性测试[J]. 康鑫,周颢,赵保华. 计算机工程. 2007(18)
[4]集成IS-IS路由选择协议的研究[J]. 康京山,韩春刚. 无线电通信技术. 2007(02)
[5]基于着色petri网的安全协议验证方法[J]. 刘进,陈丹,肖德宝. 华中师范大学学报(自然科学版). 2006(03)
[6]IS-IS路由协议一致性测试的研究与实现[J]. 范炜玮,苏金树,彭伟. 计算机工程与科学. 2006(07)
[7]OSPF和集成IS-IS路由协议的深入研究[J]. 张浩锋. 广东通信技术. 2004(12)
[8]大型IP网络IS-IS路由规划与设计[J]. 王香刚. 深圳信息职业技术学院学报. 2004(01)
[9]网络协议描述和验证技术的分析与比较[J]. 冷淑霞,徐涛. 山东理工大学学报(自然科学版). 2004(02)
硕士论文
[1]基于时间着色Petri网的SIP协议形式化验证与分析[D]. 马元飞.内蒙古大学 2012
[2]基于CPN的BitTorrent协议激励机制研究[D]. 马燕林.内蒙古大学 2012
[3]协议可扩展属性测试方法的研究与实现[D]. 郭亚杰.内蒙古大学 2012
[4]基于IS-IS路由协议的数据通信网络拓扑发现方法的设计与实现[D]. 马俐敏.北京邮电大学 2011
[5]基于着色Petri网的LDP协议验证研究[D]. 萨仁高娃.内蒙古大学 2010
[6]IS-IS路由协议一致性测试的研究[D]. 刘莹泽.内蒙古大学 2008
[7]IS-IS路由性能监测系统设计与实现[D]. 王卫华.北京邮电大学 2008
[8]集成IS-IS协议在T比特路由器中研究与实现[D]. 周建林.中国人民解放军信息工程大学 2005
[9]IS-IS协议路由计算方法的研究和实现[D]. 范炜玮.国防科学技术大学 2004
[10]中间系统—中间系统路由协议IS-IS的研究与实现[D]. 梁暾.国防科学技术大学 2004
本文编号：3200763
【文章来源】：内蒙古大学内蒙古自治区 211工程院校
【文章页数】：60 页
【学位级别】：硕士
【文章目录】：
摘要
ABSTRACT
目录
图表目录
第一章 引言
1.1 研究背景及意义
1.2 研究内容和主要工作
1.3 论文结构
第二章 背景知识介绍
2.1 IS-IS协议简介
2.2 CPN简介
2.3 CPN Tools 简介
2.4 协议验证简介
2.5 本章小结
第三章 IS-IS协议的分析
3.1 IS-IS路由协议数据的类型和建模的数据类型
3.2 IS-IS 路由协议数据的结构和建模中数据包的结构
3.3 IS-IS 路由协议功能
3.3.1 子网相关功能
3.3.2 子网独立功能
3.4 本章小结
第四章 IS-IS路由协议的形式化建模
4.1 CPN模型的抽象
4.2 数据建模
4.3 CPN层次化建模
4.3.1 TOP层模型
4.3.2 子网相关功能接收子模块
4.3.3 子网独立功能的接收进程模块
4.3.4 子网独立功能的更新进程模块
4.3.5 子网独立功能的决定进程模块
4.3.6 子网独立功能的转发进程模块
4.3.7 子网相关功能的发送进程模块
4.4 本章小结
第五章 IS-IS路由协议模型验证与分析
5.1 IS-IS路由协议正确性的验证
5.2 协议属性的验证
5.2.1 DIS属性验证
5.2.2 LSP/CSNP信息引发决定进程属性验证
5.2.3 最短路径的更新属性验证
5.3 本章小结
第六章 总结和展望
6.1 总结
6.2 未来研究方向的展望
参考文献
致谢
【参考文献】：
期刊论文
[1]Sip协议的petri网建模及性能验证[J]. 杨郁州,张伟,占东生. 微计算机信息. 2010(21)
[2]基于CPN TOOLS的网络协议建模与仿真技术研究[J]. 占东生,张伟,顾明甲. 微计算机信息. 2010(13)
[3]基于层次结构的IS-IS协议一致性测试[J]. 康鑫,周颢,赵保华. 计算机工程. 2007(18)
[4]集成IS-IS路由选择协议的研究[J]. 康京山,韩春刚. 无线电通信技术. 2007(02)
[5]基于着色petri网的安全协议验证方法[J]. 刘进,陈丹,肖德宝. 华中师范大学学报(自然科学版). 2006(03)
[6]IS-IS路由协议一致性测试的研究与实现[J]. 范炜玮,苏金树,彭伟. 计算机工程与科学. 2006(07)
[7]OSPF和集成IS-IS路由协议的深入研究[J]. 张浩锋. 广东通信技术. 2004(12)
[8]大型IP网络IS-IS路由规划与设计[J]. 王香刚. 深圳信息职业技术学院学报. 2004(01)
[9]网络协议描述和验证技术的分析与比较[J]. 冷淑霞,徐涛. 山东理工大学学报(自然科学版). 2004(02)
硕士论文
[1]基于时间着色Petri网的SIP协议形式化验证与分析[D]. 马元飞.内蒙古大学 2012
[2]基于CPN的BitTorrent协议激励机制研究[D]. 马燕林.内蒙古大学 2012
[3]协议可扩展属性测试方法的研究与实现[D]. 郭亚杰.内蒙古大学 2012
[4]基于IS-IS路由协议的数据通信网络拓扑发现方法的设计与实现[D]. 马俐敏.北京邮电大学 2011
[5]基于着色Petri网的LDP协议验证研究[D]. 萨仁高娃.内蒙古大学 2010
[6]IS-IS路由协议一致性测试的研究[D]. 刘莹泽.内蒙古大学 2008
[7]IS-IS路由性能监测系统设计与实现[D]. 王卫华.北京邮电大学 2008
[8]集成IS-IS协议在T比特路由器中研究与实现[D]. 周建林.中国人民解放军信息工程大学 2005
[9]IS-IS协议路由计算方法的研究和实现[D]. 范炜玮.国防科学技术大学 2004
[10]中间系统—中间系统路由协议IS-IS的研究与实现[D]. 梁暾.国防科学技术大学 2004
本文编号：3200763
本文链接：https://www.wllwen.com/guanlilunwen/ydhl/3200763.html
