A verified sliding window protocol with variable flow control

ABSTRACT

We present a verified sliding window protocol which uses modulo-N sequence numbers to achieve reliable flow-controlled data transfer between a source and a destination. Communication channels are assumed to lose, duplicate and reorder messages in transit. The destination's data needs are represented by a receive window whose size can vary with time. The destination entity uses acknowledgement messages to inform the source entity of the current receive window size and the sequence number of the data word next expected. The source entity responds by sending segments of data words that lie within the allowed window. Each data segment is accompanied by an identifying sequence number and the size of the data segment. The destination entity also uses selective acknowledgement and selective reject messages to inform the source entity of the reception or lack of reception, respectively, of out-of-sequence data segments. Thus, this protocol is a proper extension of the Arpanet's TCP. We have obtained the minimum value of N that ensures correct data transfer and flow control, in terms of the minimum message transmission time, the maximum message lifetime, and the maximum receive window size. The protocol imposes no constraints on the retransmissions of messages or on the data segment sizes; thus, any retransmission policy that optimizes the protocol's performance can be used.

REFERENCES

• 1: CCITT, Draft revised CCITT recommendation X.25, February 1980.
• 2: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 3: DiVlto, B. L,, "Mechanical verification of EL data transport p,'otoeol," Proe. ACM SIGCOMM '83, Austin, Texas, pp. 30-37, March 108a.
• 4: Hailpern, B. T. and S. S. Owicki, "Modular verification of computer communication protocols," IEEE T~'ans. on Common., COM-31, 1, January 1083.
• 5: Misre, J. and K. M. Chandy, "Prooh of Networks of Processes," IEEE Trans. Soft. E~g., Vol. SE-7, No. 4, July 1081.
• 6: Jon Postel, DOD standard transmission control protocol, ACM SIGCOMM Computer Communication Review, v.10 n.4, p.52-132, October 1980 [doi>10.1145/1040132.1040134]
• 7: Shankar, A. U. and S. S. Lam, "Time-dependent communleation protocols," Tutorial: Principles of Communication and Networking Protocols, S. S. Lain (ed.), IEEE Computer Society, 1984.
• 8: A. U Shankar , Simon S. Lam, Time-Dependent Distributed Systems: Proving Safety, Liveness and Real-TimeProperties, University of Texas at Austin, Austin, TX, 1985
• 9: Shankar, A. U. and S. S. Lain, "Construction of sliding window protocols by stepwise refinement," Tech. Rep. CS-TR-1647, Computer Science Dept., Univ. of Maryland, February 1980.
• 10: Shankar, A. U., "Verification of a time-dependent data transfer protocol," Tech. Rep., Computer Science Dept., Univ. of Maryland, (in preparation)
• 11: Lansing Sloan, Mechanisms that enforce bounds on packet lifetimes, ACM Transactions on Computer Systems (TOCS), v.1 n.4, p.311-330, Nov. 1983 [doi>10.1145/357377.357382]
• 12: Stenning, N. V., "A data transfer protocol," Computer Networks, Vol. 1, pp. 99-110, September 1976.

INDEX TERMS

Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
  C.2 COMPUTER-COMMUNICATION NETWORKS

General Terms:
Performance, Reliability, Standardization, Verification