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.

In this paper, it is proven that the following three decision problems on validation of protocols with bounded capacity channels are NP-complete. (1) Given a protocol with the channel capacity being 1, determine whether or not there exist deadlocks in the protocol. (2) Given a protocol with the channel capacity being 1, determine whether or not there exist unspecified receptions in the protocol. (3) Given a protocol with the channel capacity being 2, determine whether or not there exist overflows such that the channel capacity is not bounded by 1 in the protocol. These results suggest that, even when all channeles in a protocol are bounded by 1 or 2, protocol validation should be in general interactable. It also clarifies the boundary of computational complexity of protocol validation problems because the channel capacity 0 does not allow protocols to transmit and recieve messages.