HMIPv6 Formal Verification Research Based On Color Petri Nets

With the rapid development of Internet, network protocol standards are constantly updated and improved. How to effectively improve the network services has become one of key problems of the network protocol engineering field. As an extension of mobile IPv6 (MIPv6), Hierarchical mobile IPv6 (HMIPv6) is made to improve the MN (mobile nodes) fast-moving in a small range region based on MIPv6 (Mobile IPv6).CPN (Coloured Petri Nets) is a formal modeling language, which is suitable for describing a system with concurrency and communication.The CPN provides a formal description method, which is more intuitive and graphical for the users. And the CPN modeling language is a general-purpose modeling language.In this thesis, a formal model is given for the HMIPv6 protocol which has been description by natural language, and the basic properties of HMIPv6 protocol model is verified. Because of the state explosion problem caused by concurrent behavior, verification has been hindered. So a simplified and abstract method is presented. By this method, the model is simplified into multiple concurrent sub-models, and the abstraction level of concurrent sub-models is improved, some of the places and transitions are merged. So the state space is reduced and a sound verification effect is gained. Finally, these method is used on HMIPv6 model, the effectiveness of this method is testified.