Proof of Correctness of Proposed ATM Retransmission Scheme

: The CCITT has proposed a poll-based retransmission scheme as part of the Service Specific Connection Oriented Protocol for ATM systems. The basic scheme consists of the source periodically sending polls to the destination indicating which frames have been sent, and the destination responding with a status message indicating which of these frames have not been received. Many additional features have been included in the scheme in order to reduce the retransmission delay and prevent unnecessary retransmissions. With the added complexity of these features, it is not readily apparent whether the scheme generates the necessary retransmissions. We formally prove that the scheme does eventually generate a retransmission of any lost frame without producing any unnecessary retransmissions, assuming that certain reasonable conditions hold. In proving the correctness of the scheme, we also further define the protocol. We also examine how the protocol can fail if the conditions for proper operation are not met.