Advertisement

How Stop and Wait Protocols Can Fail over the Internet

  • Jonathan Billington
  • Guy Edward Gallasch
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)

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 protocol 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 parameterized 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 prove 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 

References

  1. 1.
    CCITT Recommendation Z.100, Functional Specification and Description Language (SDL) (2002) Google Scholar
  2. 2.
    FSM Library, AT&T Research Labs, http://www.research.att.com/sw/tools/fsm/
  3. 3.
    Internet Engineering Task Force, http://www.ietf.org
  4. 4.
    Aziz Abdulla, P., Jonsson, B.: Verifying Programs with Unreliable Channels. Information and Computation 127(2), 91–101 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Afek, Y., Brown, G.M.: Self-Stabilization of the Alternating Bit Protocol. In: Proceedings of the 8th Symposium on Reliable Distributed Systems, pp. 80–83. IEEE Comput. Soc. Press, Los Alamitos (1989)CrossRefGoogle Scholar
  6. 6.
    Barrett, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)Google Scholar
  7. 7.
    Billington, J.: Formal specification of protocols: Protocol Engineering. In: Encyclopedia of Microcomputers, vol. 7, pp. 299–314. Marcel Dekker, New York (1991)Google Scholar
  8. 8.
    Billington, J., Gallasch, G.E.: An Investigation of the Properties of Stop-and-Wait Protocols over Channels which can Re-order messages. Technical Report 15, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Australia (2003) Google Scholar
  9. 9.
    Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Comput. Networks and ISDN Sys. 14(1), 25–59 (1987)CrossRefGoogle Scholar
  10. 10.
    Budkowski, S., Dembinski, P.: An Introduction to Estelle: A Specification Language for Distributed Systems. Comput. Networks and ISDN Sys. 14(1), 3–23 (1987)CrossRefGoogle Scholar
  11. 11.
    Vissers, C.A., Logrippo, L.: The Importance of the Service Concept in the Design of Data Communications Protocols. In: Protocol Specification, Testing and Verification, V, pp. 3–17. North Holland, Amsterdam (1986)Google Scholar
  12. 12.
    CCITT. ISDN user-network interface data link layer specification. Technical report, Draft Recommendation Q.921, Working Party XI/6, Issue 7 (January 1984) Google Scholar
  13. 13.
    Clarke, E.M., Wing, J.M.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys 28(4), 626–643 (1996)CrossRefGoogle Scholar
  14. 14.
    CPN ML: An Extension of Standard ML, http://www.daimi.au.dk/designCPN/sml/cpnml.html
  15. 15.
    Diaz, M.: Modelling and Analysis of Communication and Co-operation Protocols Using Petri Net Based Models. In: Protocol Specification, Testing and Verification. North-Holland, Amsterdam (1982)Google Scholar
  16. 16.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall International Editions, Englewood Cliffs (1991)Google Scholar
  17. 17.
    ITU-T. Recommendation X.210, Information Technology - Open Systems Interconnection - Basic Reference Model: Conventions for the Definition of OSI Services (November 1993) Google Scholar
  18. 18.
    Billington, J., Wheeler, G.R., Wilbur-Ham, M.C.: PROTEAN: A High-level Petri Net Tool for the Specification and Verification of Communication Protocols. In: IEEE Transactions on Software Engineering, vol. 14, pp. 301–316. IEEE Press, Los Alamitos (1988)Google Scholar
  19. 19.
    Billington, J., Diaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)Google Scholar
  20. 20.
    Billington, J., Wilbur-Ham, M.C., Bearman, M.Y.: Automated Protocol Verification. In: Protocol Specification, Testing and Verification, V, pp. 59–70. North Holland, Amsterdam (1986)Google Scholar
  21. 21.
    Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Basic Concepts, vol. 1. Springer, Heidelberg (1992)CrossRefzbMATHGoogle Scholar
  22. 22.
    Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A Note on Reliable Full-Duplex Transmission over Half-Duplex Links. Communications of the ACM 12(5), 260–261 (1969)CrossRefGoogle Scholar
  23. 23.
    Kristensen, L.M., Christensen, S., Jensen, K.: The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer 2(2), 98–132 (1998)CrossRefzbMATHGoogle Scholar
  24. 24.
    Standard ML of New Jersey, http://cm.bell-labs.com/cm/cs/what/smlnj/
  25. 25.
  26. 26.
    Reisig, W.: Elements of Distributed Algorithms: Modelling and Analysis with Petri Nets, vol. 4. Springer, Heidelberg (1998)CrossRefzbMATHGoogle Scholar
  27. 27.
    Stallings, W.: Data and Computer Communications, 6th edn. Prentice Hall, Englewood Cliffs (2000)zbMATHGoogle Scholar
  28. 28.
    Steggles, L.J., Kosiuczenko, P.: A Timed Rewriting Logic Semantics for SDL: a case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science 15 (1998)Google Scholar
  29. 29.
    Suzuki, I.: Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)CrossRefGoogle Scholar
  30. 30.
    Suzuki, I.: Specification and Verification of the Alternating Bit Protocol by Temporal Petri Nets. In: Proceedings of the 32nd Midwest Symposium on Circuits and Systems. IEEE Press, Los Alamitos (1990)Google Scholar
  31. 31.
    Tanenbaum, A.: Computer Networks, 4th edn. Prentice Hall, Englewood Cliffs (2003)zbMATHGoogle Scholar
  32. 32.
    The Internet Engineering Task Force. Transmission Control Protocol. RFC 793 (1981) Google Scholar
  33. 33.
    The Internet Engineering Task Force. TCP Extensions for High Performance. RFC 1323 (1992) Google Scholar
  34. 34.
    Turner, K.J. (ed.): Using Formal Description Techniques: An Introduction to Estelle, Lotos and SDL. John Wiley & Sons, Chichester (1993)Google Scholar
  35. 35.
    Wing, J.M.: A Specifier’s Introduction to Formal Methods. IEEE Computer 23(9), 8–24 (1990)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Jonathan Billington
    • 1
  • Guy Edward Gallasch
    • 1
  1. 1.Computer Systems Engineering CentreUniversity of South AustraliaAustralia

Personalised recommendations