CPN Modeling and Analysis of HMIPv6

Hierarchy Mobile IPv6 (HMIPv6) is a scheme for micro mobility management to help basic Mobile IP reduce the signal cost and the packet loss during the periods of handover. In this paper, we describe and analyze the protocol based on, instead of the conventional ways of message sequence charts, but the Colored Petri Net (CPN). CPN is suitable to model a system from the dynamic perspective and has the ability to analyze it in a formal way. The CPN based modeling of HMIPv6 is built in this paper, highlighting the mechanism of packet forwarding and micro mobility management. The model is also analyzed by means of the occurrence graph (OG), through which we find an exceptional state would cause packet loss in the seamless handover algorithm used in HMIPv6.