Vertification Of OSPF Protocol Based On Coloured Petri Net

The computer network is one of the rapidly developing computer techniques nowadays. The core to guarantee the network work normally is computer network protocol. Protocol is spirit of computer network. The rapid increasement of protocol complexity results in a discipline of protocol engineering. This paper mainly introduces the protocol verification and analysis of protocol engineering activities, expounds the purpose and method of protocol verification, then analysis the protocol model technology in common use, and introduce the protocol verification based on FSM and Petri Nets model.OSPF protocol is classified as an Interior Gateway Protocol, which is a dynamic routing protocol. Each OSPF router maintains an identical link-state database describing the Autonomous System' s topology. From this database, a routing table is calculated by constructing a shortest_ path tree. In this paper, coloured Petri net model of calculating the shortest-path tree for an area is given. CPN tool designed by myself can be used to produce occurrence graph for CPN model. Consequently, OSPF protocol can be verification.