Validation of the Detailed Design of the Label Distribution Protocol for the Multiprotocol Label Switching System
Summary :
In this paper, we describe the development and the analysis of the Label Distribution Protocol (LDP) for Multiprotocol Label Switching System. We review the implementation issues that are required to construct the LDP for a gigabit switched router and propose a detailed design of the LDP. We present the detailed design using the Deviation Tree of the protocol state machine and a formal specification of the state machine using the process algebra. These specifications are based on the IETF standard. By analyzing the protocol behaviors of the Deviation Trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP. We expect that the reliability would be improved using these analyses. With these proofs we expect the implemented LDP will be interoperable with other commercialized products. As a result we validate the protocol behaviors of the implemented LDP.
- Publication
- IEICE TRANSACTIONS on Communications Vol.E86-B No.2 pp.506-517
- Publication Date
- 2003/02/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Internet Technology III)
- Category
- MPLS and Routing
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Jae-Hyun PARK, "Validation of the Detailed Design of the Label Distribution Protocol for the Multiprotocol Label Switching System" in IEICE TRANSACTIONS on Communications,
vol. E86-B, no. 2, pp. 506-517, February 2003, doi: .
Abstract: In this paper, we describe the development and the analysis of the Label Distribution Protocol (LDP) for Multiprotocol Label Switching System. We review the implementation issues that are required to construct the LDP for a gigabit switched router and propose a detailed design of the LDP. We present the detailed design using the Deviation Tree of the protocol state machine and a formal specification of the state machine using the process algebra. These specifications are based on the IETF standard. By analyzing the protocol behaviors of the Deviation Trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP. We expect that the reliability would be improved using these analyses. With these proofs we expect the implemented LDP will be interoperable with other commercialized products. As a result we validate the protocol behaviors of the implemented LDP.
URL: https://global.ieice.org/en_transactions/communications/10.1587/e86-b_2_506/_p
Copy
@ARTICLE{e86-b_2_506,
author={Jae-Hyun PARK, },
journal={IEICE TRANSACTIONS on Communications},
title={Validation of the Detailed Design of the Label Distribution Protocol for the Multiprotocol Label Switching System},
year={2003},
volume={E86-B},
number={2},
pages={506-517},
abstract={In this paper, we describe the development and the analysis of the Label Distribution Protocol (LDP) for Multiprotocol Label Switching System. We review the implementation issues that are required to construct the LDP for a gigabit switched router and propose a detailed design of the LDP. We present the detailed design using the Deviation Tree of the protocol state machine and a formal specification of the state machine using the process algebra. These specifications are based on the IETF standard. By analyzing the protocol behaviors of the Deviation Trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP. We expect that the reliability would be improved using these analyses. With these proofs we expect the implemented LDP will be interoperable with other commercialized products. As a result we validate the protocol behaviors of the implemented LDP.},
keywords={},
doi={},
ISSN={},
month={February},}
Copy
TY - JOUR
TI - Validation of the Detailed Design of the Label Distribution Protocol for the Multiprotocol Label Switching System
T2 - IEICE TRANSACTIONS on Communications
SP - 506
EP - 517
AU - Jae-Hyun PARK
PY - 2003
DO -
JO - IEICE TRANSACTIONS on Communications
SN -
VL - E86-B
IS - 2
JA - IEICE TRANSACTIONS on Communications
Y1 - February 2003
AB - In this paper, we describe the development and the analysis of the Label Distribution Protocol (LDP) for Multiprotocol Label Switching System. We review the implementation issues that are required to construct the LDP for a gigabit switched router and propose a detailed design of the LDP. We present the detailed design using the Deviation Tree of the protocol state machine and a formal specification of the state machine using the process algebra. These specifications are based on the IETF standard. By analyzing the protocol behaviors of the Deviation Trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP. We expect that the reliability would be improved using these analyses. With these proofs we expect the implemented LDP will be interoperable with other commercialized products. As a result we validate the protocol behaviors of the implemented LDP.
ER -
English
