| 基于Uppaal的移动IPv6协议的模型检测 |
| |
| 引用本文： | 张冬梅,马华东,高大永.基于Uppaal的移动IPv6协议的模型检测[J].北京邮电大学学报,2005,28(4):45-49. |
| |
| 作者姓名： | 张冬梅 马华东 高大永 |
| |
| 作者单位： | 北京邮电大学,计算机科学与技术学院,北京,100876;北京邮电大学,计算机科学与技术学院,北京,100876;北京邮电大学,计算机科学与技术学院,北京,100876 |
| |
| 摘 要： | 采用形式化方法对移动IPv6协议系统建立了时间自动机模型，使用实时模型检测工具Uppaal对所建模型的关键性质：活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因，提出了移动IPv6实现平滑切换的理想时间约束条件，并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.
|
| 关 键 词： | 移动性 形式化描述 模型检测 |
| 文章编号： | 1007-5321（2005）04-0045-05 |
| 收稿时间： | 2004-06-08 |
| 修稿时间： | 2004年6月8日 |
Automatic Verification of Mobile IPv6 Using Uppaal |
| |
| ZHANG Dong-mei,MA Hua-dong,GAO Da-yong.Automatic Verification of Mobile IPv6 Using Uppaal[J].Journal of Beijing University of Posts and Telecommunications,2005,28(4):45-49. |
| |
| Authors: | ZHANG Dong-mei MA Hua-dong GAO Da-yong |
| |
| Affiliation: | School of Computer Science and Technology, Beijing University of Posts and Telecommunications, Beijing 100876, China |
| |
| 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. |
| |
| Keywords: | mobility formal specification model-checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《北京邮电大学学报》浏览原始摘要信息 |
|
点击此处可从《北京邮电大学学报》下载全文 |
|
