OSPFv3 protocol simulation with colored Petri nets

OSPF is the most popular interior gateway protocol proposed by IETF to distribute routing information among routers belonging to the same autonomous system. OSPF for IPv6, also referred to as OSPFv3, has been widely researched and implemented by many manufacturers in various devices such as routers and operation systems. Since IPv6 has been regarded as the kernel protocol of the next generation Internet, conformance of all OSPFv3 implementation with protocol specification is the premise to guarantee the interoperability between various routing devices. Protocol conformance test system (PCTS) is used for verifying whether the implementation under test (IUT) conforms to protocol specification. How to generate complete test cases is one of the most important issues in PCTS. In this paper, after analyzing the mechanism of OSPFv3, we use CPNs to model the main features of this complex protocol. The construction of this CPN model is presented, and the state space analysis is given based on the occurrence graph.