A full-duplex DLC protocol on two links

The authors consider a special case of multilink protocol, namely, a system consisting of two half-duplex parallel links that carry data in opposite directions between two nodes. They construct a protocol that simulates a full-duplex reliable link between the two nodes. Synchronization is achieved without resorting to the use of serial numbers. A validation proof of the protocol is provided. The design of the protocol exhibits an instance of the value of correctness proofs in the design process, as several successive protocols, discussed in the paper, were only found to be incorrect through the effort to prove them otherwise