Title :
Research on the LDP Protocol Verification Based on Coloured Petri Nets
Author :
Rengaowa, Sa ; Zhao Yulan ; Hai Chunmei
Author_Institution :
Comput. & Inf. Eng. Coll., Inner Mongolia Normal Univ., Hohhot, China
Abstract :
A CPN model for the LDP protocol under the specific configuration mode (using downstream on demand label distribution, LSP ordered control, conservative label retention and non VC-merge mode) has been designed and implemented .Then using the 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.
Keywords :
Petri nets; formal logic; protocols; ASK-CTL; LDP protocol verification; LSP ordered control; branching temporal logic; coloured Petri nets; conservative label retention; demand label distribution; label distribution process; nonVC-merge mode; Analytical models; Forward error correction; Image color analysis; Multiprotocol label switching; Routing; Switches;
Conference_Titel :
Internet Technology and Applications, 2010 International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-5142-5
Electronic_ISBN :
978-1-4244-5143-2
DOI :
10.1109/ITAPP.2010.5566261
