Research On The LDP Protocol Verification Based On Coloured Petri Nets

The features of network protocols,such as distributed, concurrency and asynchronous, have brought a great challenge to the quality of the network protocol development. The protocol verification is a process to check protocol functions and performance and it is essential link to guarantee the quality of protocol development. The premise of protocol formal verification is the formal description of protocol behavior and the protocol properties.The protocol behavior is described through the formal models or the formal language. However the describing method of protocol properties uses the system assertion language (CTL,ASK-CTL etc).Model checking is a formalized verification method. It can automatically verify whether a system is meeting their specifications. It is widely used in hardware, software and protocol verifications.Through the protocol model people can master the protocol macroscopically and in whole.And also can discover the problems or the omissions early. The protocol model provides basic ideas for the code generation of protocol implementation and gives the template guide to construct the system of protocol mplementation. MPLS (Multiprotocol Label Switching) is one of the new network technologies that come along with the development of Internet. MPLS forwards packet using simple fixed-length labels;it combines complex and flexible routing protocol in the traditional network layer with inexpensive high-speed switching hardware in data link layer. LDP is a new protocol defined for the explicit purpose of distributing labels in MPLS technology.Based on the analyzing of LDP protocol,a CPN model for the LDP protocol under the specific configuration mode has been designed and implemented with CPN Tools in this thesis.Then using the State Space Tool of CPN tools has simulated and analyzed the LDP protocol based on its CPN model and then obtained the protocol analysis report. Finally, using a CTL like branching temporal logic ASK-CTL, has verified that label distribution process of the LDP protocol and validated its property of establishing label switched path LSP under the specific configuration mode; and all the places of the LDP protocol model are bounded, all the transitions are fair transitions, and has two terminal markings.