Lecture Notes in Computer Science (LNCS) 2767, Springer-Verlag, 209-223 pages, 2003.
Abstract: The correct operation of computer protocols is essential to the smooth operation of the distributed systems that facilitate our global economy. Formal techniques provide our best chance to ensure that protocols designs are free from errors. This invited paper revisits the class of Stop-and-Wait protocols that incorporate retransmission strategies to recover from transmission errors. This is motivated by the fact that their basic mechanisms are important for practical protocols such as the Internet's Transmission Control Protocol (TCP). Stop-and-Wait protocols have been shown to operate correctly over media that may lose packets, however, there has been little discussion regarding the operation of these protocols over media that can re-order packets. The paper presents an investigation of these protocols operating over a medium, such as that provided by the Internet Protocol, that does allow reordering of data. Coloured Petri Nets are used to build a model of a Stop-and-Wait Protocol parameterised by its maximum sequence number and the maximum value of the retransmission counter. The model is analysed using a combination of hand proofs and automatic techniques. We identify four problems. We firstly provide the counter intuitive property for a Stop-and-Wait protocol that the number of packets that are stored in the network can grow without bound. This is true for any positive values of the maximum sequence number and the maximum number of retransmissions. We further show that loss of packets is possible and that duplicates can be accepted as new packets by the receiver. These first three properties hold even though the sender and receiver perceive that the protocol is operating correctly. The final problem is that the protocol does not satisfy the Stop-and-Wait service where sends and receives alternate. Finally, we provide a discussion of the relevance of these results to the Transmission Control Protocol.
Keywords: Stop and Wait Protocols; TCP State space methods; Coloured Petri Nets; Protocol Analysis and Verification.