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

fYear

2010

fDate

20-22 Aug. 2010

Firstpage

1

Lastpage

4

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ITAPP.2010.5566261

Filename

5566261