【摘要】 采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质:活性、移动性和平滑切换等进行了分析和检测.检测结果证明,移动IPv6协议在切换时存在丢包现象.通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质.结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.更多还原

【Abstract】 A timed automata model of mobile Internet protocol version 6 (IPv6) using formal method was presented, and the protocol’s key properties of liveness, mobility and seamless handoff were verified by the real-time model checker Uppaal. The verification proves that the packet loss occurs during the period of handoff process. An ideal condition guaranteeing the seamless handoff is proposed by analyzing the reason of packet loss, and in this condition, the verification shows that the property of seamless handoff of mobile IPv6 is satisfied. Some suggestions that are likely to lead to mobility performance improvement for mobile IPv6 are given.更多还原