10.3969/j.issn.1007-5321.2005.04.011
基于Uppaal的移动IPv6协议的模型检测
采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质:活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.
移动性、形式化描述、模型检测
28
TP393.4(计算技术、计算机技术)
国家自然科学基金60242002
2005-11-03(万方平台首次上网日期,不代表论文的发表时间)
共5页
45-49