HMIPv6 Formal Verification Research Based On Color Petri Nets

Hierarchical mobile IPv6 (HMIPv6) is made to improve the MN (mobile nodes) fast-moving in a small range region based on MIPv6 (Mobile IPv6). HMIPv6 gives a solution for MIPv6 dealing with the movement in a large range region and the movement in a small range region the same scheme, but the MN fast moving within a small range region will bring update packets switching frequently. HMIPv6 hierarchically divides the network. HMIPv6 introduce a new entity-mobile anchor point (MAP) in each region, MAP divides the mobile node's movement into "Macro Mobility" and "Micro Mobility", which improves the basic MIPv6 handover scheme for reducing packets loss and transmission delay during mobility and improves the communication quality.Formal verification for the HMIPv6 protocol can not only gives a formal specification describes, provides a basis protocol model for follow-up improvement, facilitates the analysis of improving the protocol, and provides a credible guarantee for the realization of the software. This thesis analyses the HMIPv6 protocol, extracts properties based on events; using hierarchical modeling method and "universal module" idea,we give a CPN (Color Petri Nets) hierarchical model of HMIPv6 protocol. Using the integrated method, we verify that the model fulfill the requirements of HMIPv6 protocol by simulated execution, the state space report, all state space analysis, ASKCTL model checking. The CPN is combination of a graphical language and effective formal model. CPN simulates intuitively and has strong advantages in describing the complex data, hierarchical modeling, concurrency, communication, and synchronization.