学位论文 > 优秀研究生学位论文题录展示

HMIPv6协议形式化建模及测试例生成方法研究

作　者: 杨蒙
导　师: 叶新铭
学　校: 内蒙古大学
专　业: 计算机科学与技术
关键词: HMIPv6协议形式化建模 Coloured Petri Nets 属性测试例生成
分类号: TN915.04
类　型: 硕士论文
年　份: 2010年
下　载: 15次
引　用: 1次
阅　读: 论文下载

内容摘要

随着网络通信技术的高速发展,网络协议标准也不断地更新和完善。如何更有效地保证网络协议的实现质量,已成为网络协议工程领域的关键问题之一。实践证明,以合理有效的方式将形式化方法应用于协议研发实践中,可以有效提高协议设计、实现、测试的效率,最大程度地保证协议实现的正确性。协议一致性测试用于检查协议实现是否符合协议设计的要求,是保障协议实现质量的有效方法。HMIPv6协议作为移动IPv6协议的优化,在行为特性、安全性等方面采用了新的技术。如何借助于形式化方法对此协议进行有效的一致性测试成为亟待解决的问题。本文采用Coloured Petri Nets对HMIPv6协议进行形式化建模,并且使用了层次化的建模方法,将HMIPv6协议按节点类型抽象成若干层,层次化的模型不但更能体现不同节点间的交互属性,而且由于层次间的相对独立性,使得模型的开发更加模块化。此类通信协议的特点是并发度较高,且交互行为较多,Coloured Petri Nets非常适合于描述具有这些特点的系统。CPN tools还支持模型相关性质的分析,从而保证了模型的正确性。在一致性测试方法上,本文提出了由协议属性指导的测试例生成。文中对属性也采用Coloured Petri Nets进行形式化描述,给出了基于属性的测试例生成算法。该算法使得测试例的生成过程简单,直接,且针对性强。算法的提出使得测试例自动生成成为可能,本文作者开发了基于CPNs的测试例生成工具,重点实现了本文提出的属性指导的测试例生成算法,实现了测试例生成的自动化,取得了良好的测试效果。

全文目录

摘要  4-6
ABSTRACT  6-12
第一章引言  12-15
  1.1 研究背景  12-13
  1.2 论文的创新性和主要工作概述  13
  1.3 论文的整体结构和章节安排  13-15
第二章 HMIPv6协议概述  15-25
  2.1 相关术语  16-17
  2.2 HMIPv6协议概述  17-19
  2.3 移动IPv6扩展-本地绑定更新  19-20
  2.4 邻居发现扩展-MAP选项  20-21
  2.5 HMIPv6协议操作  21-23
    2.5.1 移动节点操作  21-23
      2.5.1.1 发送数据包到通信节点  22-23
    2.5.2 MAP操作  23
  2.6 本章小结  23-25
第三章 Coloured Petri Nets  25-34
  3.1 CPNs概述  25-26
  3.2 CPNs的形式化定义  26-28
  3.3 CPN Tools  28-29
  3.4 与其他形式化描述技术的比较  29-32
  3.5 本章小结  32-34
第四章 HMIPv6协议的CPNs模型  34-42
  4.1 数据模型  34-35
  4.2 宏移动模型  35-39
  4.3 微移动模型  39-41
  4.4 本章小结  41-42
第五章状态空间  42-49
  5.1 状态空间简述  42
  5.2 宏移动模型状态空间  42-47
  5.3 微移动模型状态空间  47
  5.4 本章小结  47-49
第六章基于属性的测试例生成  49-73
  6.1 基于属性的测试例生成算法  50-63
    6.1.1 属性的定义  50-53
    6.1.2 属性的状态空间投影操作  53-56
    6.1.3 测试例生成算法  56-57
    6.1.4 测试例生成算法示例  57-63
  6.2 测试例自动生成工具  63-72
    6.2.1 CPNs模型的两种表现形式  63-66
    6.2.2 重构状态空间  66-69
    6.2.3 自动生成测试例  69-72
  6.3 与其他测试例生成方法的比较  72
  6.4 本章小结  72-73
第七章结束语  73-75
  7.1 论文工作总结  73
  7.2 下一步研究工作  73-75
参考文献  75-78
致谢  78

HMIPv6协议形式化建模及测试例生成方法研究

内容摘要

全文目录

相似论文