Abstract
In order to verify the correctness of the label distribution protocol LDP, a function verification model has been constructed for the protocol-integrated analysis in the aspects of safety property, liveness property, and function analysis based on the Colored Petri Nets (CPN). By this integrated analysis method using CPN, it has been confirmed that the protocol can adapt to changes in the network layer routing information and distribute labels effectively. Also, this CPN-based modeling and simulation method, which integrates the protocol property verification and function analysis, contributes a significant methodology to improve the function of a network protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Guo XQ. Research on conformance testing of LDP protocol based on E-LOTOS. Master’s degree thesis of Inner Mongolia University, Hohhot, China. 2012, (In Chinese).
Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of the workshop on tools and algorithms for the construction and analysis of systems (TACAS’ 99). Lecture notes in computer science, vol. 1579. Berlin: Springer; 1999. pp. 193–207.
Rosen E. Multiprotocol label switching architecture. 2001. http://www.ietf.org/rfc/rfc3031.txt. Accessed January 2001.
Andersson L. LDP specification. 2001. http://www.ietf.org/rfc/rfc3036.txt. Accessed January 2001.
Zhang J, Liu J, Ye XM, Xu ZJ. Modeling and simulation of trusted router discovery protocol using colored Petri nets. J Syst Sim. 2012;24(3):701–9 (In Chinese).
Liu J, Ye XM, Li J. Towards formal modeling methodology of BitTorrent based on Petri nets. J Syst Sim. 2011;23(11):2312–20 (In Chinese).
Li H. Research on network protocol modeling and interoperability testing based on property. Doctor dissertation of Inner Mongolia University, Hohhot, China. 2010, (In Chinese).
Wang YY. Research on web composition services model verification and testing technique based on timed color Petri nets. Doctor dissertation of Xidian University, Xi’an. 2012, (In Chinese).
Acknowledgements
This research is supported by the Natural Science Foundations of China (No. 61167004 and 61205127) and construction funds of the technology innovation team of Computer and Information Engineering College of Inner Mongolia Normal University.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Sa, R., Xilin, B., Zhao, Y., Menke, N. (2015). The LDP Protocol Formal Description and Verification Based on CPN Model. In: Wong, W. (eds) Proceedings of the 4th International Conference on Computer Engineering and Networks. Lecture Notes in Electrical Engineering, vol 355. Springer, Cham. https://doi.org/10.1007/978-3-319-11104-9_36
Download citation
DOI: https://doi.org/10.1007/978-3-319-11104-9_36
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11103-2
Online ISBN: 978-3-319-11104-9
eBook Packages: EngineeringEngineering (R0)