HMIPv6 Protocol Formal Modeling And Research On Test Case Generation Method

With the rapid development of network communication technology, network protocol standards are constantly updated and improved. How to ensure the quality of the implementations of the protocols has become one of the key problems of the network protocol engineering field. Practices show that formal methods can efficiently improve the efficiency of the protocol developing process and the quality of protocol. Protocol conformance testing is an effective way to check weather the implementations conform the specification.As an improvement of mobile IPv6 protocol, HMIPv6 protocol adopts new technologies in behavior characteristics, safety and other aspects. It becomes an urgent problem to test HMIPv6 protocol effectively with formal method.In this thesis, Coloured Petri Nets is used to model the HMIPv6 protocol. The model divides HMIPv6 protocol into several hierarchies according to the type of the nodes. The hierarchical model not only better reflects the interaction properties between the different nodes, but also makes the process of modeling is modularized. CPN Tools can be used to analyze the properties of the model.In this thesis, test case generation is conducted by the property which is defined with Coloured Petri Nets. Test case generation method based on property is given. This method makes the process of test case generation more simply, directly, and pointed. The author of this thesis also develops the test case generation tools. The efficiency of test case generation is improved immensely with the employment of the tools.