基于Uppaal的移动IPv6协议的模型检测

摘要

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