关键词: 移动性, 形式化描述, 模型检测

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