%0 Journal Article
%T 基于Uppaal的移动IPv6协议的模型检测
%A 张冬梅
%A 马华东
%A 高大永
%J 北京邮电大学学报
%P 45-49
%D 2005
%R 10.13190/jbupt.200504.45.zhangdm
%X 采用形式化方法对移动IPv6协议系统建立了时间自动机模型，使用实时模型检测工具Uppaal对所建模型的关键性质活性、移动性和平滑切换等进行了分析和检测.检测结果证明,移动IPv6协议在切换时存在丢包现象.通过分析丢包产生的原因，提出了移动IPv6实现平滑切换的理想时间约束条件，并在理想条件下重新验证了协议的性质.结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.
%K 移动性
%K 形式化描述
%K 模型检测
%U http://www.buptjournal.cn/CN/abstract/abstract1590.shtml