论文部分内容阅读
IETF在移动IPv6(MIPv6)的基础上针对移动节点在小范围内快速移动提出了一种改进技术,即层次化移动IPv6(HMIPv6)技术。它通过引入移动锚点(MAP),对网络进行了层次化划分,使移动节点的移动行为分为宏移动和微移动。这改进了MIPv6的切换方案,提高了通信质量。协议一致性测试用于检查协议实现是否符合协议设计的要求,是保障协议实现质量的有效方法。Coloured Petri Nets(CPN)非常适合于描述具有并发和通信的系统。CPN Tools还支持模型相关性质的分析。TTCN-3是一种功能强大的测试标准语言。如何结合CPN和TTCN-3对HMIPv6协议进行有效的一致性测试成为亟待解决的问题。本文主要研究基于CPN和TTCN-3的HMIPv6协议一致性测试。首先,使用CPN及其仿真工具CPN Tools对HMIPv6协议进行了层次化建模,并用点火约束条件简化了模型生成的状态空间并分别生成了微移动状态空间和宏移动状态空间。然后,在系统CPN模型的基础上,对CPN属性做了形式化定义,给出了基于CPN属性的测试序列生成算法,并应用该算法开发了自动生成测试序列的工具,实现了基于CPN属性的测试序列的自动生成。最后,提出了结合CPN编写TTCN-3测试例的方法,并用这种方法编写了HMIPv6协议的TTCN-3测试例。