Service specification and protocol construction for the transport layer

ABSTRACT

In a computer network, the transport layer uses the service offered by the network layer and in turn offers its users the transport service of reliable connection management and data transfer. We provide a formal specification of the transport service in terms of an event-driven system and safety and progress properties. We construct three verified transport protocols that offer the transport service. The first transport protocol assumes a perfect network service, the second assumes loss-only network service, and the third assumes loss, reordering and duplication network service. Our transport service specifications are very realistic. Each user can be closed, listening, active opening, passive opening, open, or closing. A local incarnation number uniquely identifies every active opening and listening duration. Users can issue requests for connection, listening, closing, data send, etc. The transport layer issues indications for successful or unsuccessful connection, closing, data reception, etc. A connection is established only if one user requested the connection and the other was listening, or both requested the connection. A user receives data only from the appropriate incarnation of the distant user, and receives it insequence, without loss or duplication. Progress properties ensure that every outstanding user request is eventually responded to by an appropriate transport indication. Our protocols are constructed by stepwise refinement of the transport service. The construction method automatically generates a verification that the protocols satisfy the transport service. One distinctive feature of our protocol construction is that the events and verification of the data transfer function is directly obtained from any one of the numerous verified single-incarnation data transfer protocols already presented in the literature.

REFERENCES

• BILL: Jonathan Billington, Specification of the Transport Service Using Numerical Petri Nets, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.77-100, May 17-20, 1982
• BRNK: E. Brinksma and G. Karjoth, "A Specification of the Transport Service in LOTOS", Protocol Specification, Testing, and Verifications, IV, 1984, North-Holland, 1985.
• CCITT: CCITT, Transport Service Definition for Open Systems Interconnection (OSI) for CCITT Applications, International Telegraph and Telephone Consultative Committee Recommendation X.214, 1985.
• DIJK: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• DoD: Transmission Control Protocol, DDN Protocol Handbook: DoD Military Standard Protocols, DDN Network Information Center, SRi, MILSTD1778, Aug 1983.
• HAAS: Otto Haas, Formal protocol specification based on attribute grammars, Proceedings of the IFIP WG6.1 Fifth International Conference on Protocol Specification, Testing and Verification V, p.39-48, June 10-13, 1985
• ISO1: International Organization for Standardization, Information ?rocessiTtg Systems- Open Systems Interconnection - Transport Protocol Specification, ISO DIS S073, 1985.
• ISO2: International Organization for Standardization, A Formal Description of {SO 8073 in ESTELLE, Working draft, ISO TC 87/S0 6/WG 4 Nl4, Mar 1985.
• LAM: S.S. Lain and A. U. Shankar, "Specifying an Implementation to Satisfy Interface Specifications: A State Transition Approach," presented at the 26th Annual Lake Arrowhead workshop, Sept. 16-18, 1987.
• LOGR: L. Logrippo , D. Simon , H. Ural, Executable description of the OSI transport service in Prolog, Proc. of IFIP WG 6.1 4th Int'l Workshop on Protocol specification, testing, and verification, IV, p.279-293, June 1985, Skytop Lodge, Pennsylvania, United States
• MANN: Zohar Manna , Amir Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Science of Computer Programming, v.4 n.3, p.257-289, Dec. 1984 [doi>10.1016/0167-6423(84)90003-0]
• MUR1: S. L. Murphy , A. U. Shankar, A verified connection management protocol for the transport layer, Proceedings of the ACM workshop on Frontiers in computer communications technology, p.110-125, August 11-13, 1987, Stowe, Vermont, United States
• MUR2: S. L. Murphy and A. U. Shankar, "Service Specification and Protocol Construction for the Transport Layer," 0S-TR-2033, Dept. of Computer Science, University of Maryland, May 1988.
• SHAN1: A U Shankar, A verified sliding window protocol with variable flow control, Proceedings of the ACM SIGCOMM conference on Communications architectures & protocols, p.84-91, August 05-07, 1986, Stowe, Vermont, United States
• SHAN2: A. U. Shankar, "Verified data transfer protocols with variable flow control", CS-TR-1746, Dept. of Computer Science, University of Maryland, Mar 1987, conditionally accepted in ACM TOCS.
• SHAN3: A. Udaya Shankar , Simon S. Lam, A stepwise refinement heuristic for protocol construction, University of Maryland at College Park, College Park, MD, 1990
• SHAN4: A. U. Shankar, "A Connection Management, Protocol for the Transport Layer and Its Verification", submitted for publication.
• SIDH: D. P. Sidhu , C. S. Crall, Executable logic specifications for protocol service interfaces, IEEE Transactions on Software Engineering, v.14 n.1, p.98-121, January 1988 [doi>10.1109/32.4626]
• STEN: Stenning, N. V., "A data transfer protocol," Computer Networks, Vol. 1, pp. 99-110, September 1976.
• SUN: C.A. Sunshine and Y. K. Dalal, "Connection Management in Transport Protocols", Computer Networks, Vol.2(6), Dec 1978.
• TCP: Transmission Control Protocol, Request for Comments 793, Network Information Center, SRI International, 1981.
• VISS: Chris A. Vissers , Luigi Logrippo, The importance of the service concept in the design of data communications protocols, Proceedings of the IFIP WG6.1 Fifth International Conference on Protocol Specification, Testing and Verification V, p.3-17, June 10-13, 1985

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.3 Network Operations
          Subjects: Network management

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Data communications
      C.2.1 Network Architecture and Design
          Subjects: Distributed networks
      C.2.2 Network Protocols
          Subjects: Protocol architecture (OSI model); Protocol verification

General Terms:
Design, Theory