Automatic Verification of Mobile IPv6 Using Uppaal

doi:10.13190/jbupt.200504.45.zhangdm

JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM ›› 2005, Vol. 28 ›› Issue (4): 45-49.doi: 10.13190/jbupt.200504.45.zhangdm

• Papers • Previous Articles Next Articles

Automatic Verification of Mobile IPv6 Using Uppaal

HANG Dongmei,MA Huadong,GAO Dayong

School of Computer Science and Technology, Beijing University of Posts and Telecommunications, Beijing 100876, China

Online:2005-08-28 Published:2005-08-28

Abstract

Abstract:

A timed automata model of mobile Internet protocol version 6 (IPv6) using formalmethod 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.

Key words: mobility, formal specification, modelchecking

HANG Dongmei,MA Huadong,GAO Dayong. Automatic Verification of Mobile IPv6 Using Uppaal[J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2005, 28(4): 45-49.

[1]	WANG Guo-qing. Energy Consumption Modeling and Analysis of NDN Data Provider Mobile Support Strategies [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(2): 75-80.
[2]	XING Bing-qian, WEI Zai-xue. Time-Varying Channel Modeling and Simulation Based on 3GPP TR38.901 Channel Model [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(1): 45-51.
[3]	JIAO Ming-han, PENG Mu-gen, LIU Chen-xi. Research on Coverage and Handover Performance of Unmanned Aerial Vehicle Network [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(6): 74-81.
[4]	ZHANG Si-hai, ZHANG Jian-hua, CHEN Ying, ZHU Jin-kang. Wireless Big Data Enabled Emerging Technologies for Beyond 5G System [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2018, 41(5): 52-61.
[5]	ZHANG Guo-min, WANG Na, WANG Rui, CHEN Qiu-li, LIU Fang-xin. UAV 3D Mobility Model Based on Visit Density [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2017, 40(s1): 112-116.
[6]	ZHOU Yue-xian, WANG Bao-sheng, DENG Wen-ping, TANG Zhu, GAO Xian-ming. Mobility Support of Locator/ID Separation Protocol Based on OpenLISP [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2017, 40(s1): 117-121.
[7]	REN Fei, QIN Ya-juan, ZHOU Hua-chun, XU Ya-kun. Distributed Mobility Management in Content-Centric Networking [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2016, 39(4): 40-44,97.
[8]	JIN Yan-liang, FANG Chang-li, YAO Bin. A Combined Chirp Signal Time-Synchronization Scheme for Mobile Underwater Sensor Networks [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2016, 39(1): 52-57.
[9]	HUANG Xiao-min, WANG Yang, ZHANG Ji-liang, ZHANG Nai-tong. Performance Evaluation of VANETs Wireless Link Transmitting Data Service [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2014, 37(s1): 66-71.
[10]	LÜ Bo, WU Mu-qing, WANG Dong-yang. A Genetic Algorithm-Based Mobility Model in Social Networks [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2014, 37(1): 112-116.
[11]	ZHU Yi-hua; LI Yan-jun; YOU Li-li; PAN Jian;. An Optimal Dynamic Deployment of Paging Areas  for Mobile IP Networks [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2010, 33(3): 24-29.
[12]	LIU Yin-long,ZENG Zhi-min,XIA Hai-lun, ZHANG Tian-kui. Analysis on the Call Blocking Probability Considering Location Update Failure [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2009, 32(5): 24-27.
[13]	LU Li-hua, IU Yuan-an. Route Optimization for Nested Mobile Network in Local Mobility Domain [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2008, 31(3): 128-132.
[14]	. A Novel MAP Selection Scheme based on Minimal Average Handover Delay (MAHD-MS) in Multi-level HMIPv6 Networks [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2007, 29(s1): 70-74.
[15]	YANG Wen-chao，JIA Shi-lou. MIP Handover Time-Delay Improving Based on Hierarchical MAP [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2007, 30(2): 127-131.

Automatic Verification of Mobile IPv6 Using Uppaal

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments