A stepwise refinement heuristic for protocol construction

ABSTRACT

A stepwise refinement heuristic to construct distributed systems is presented. The heuristic is based on a conditional refinement relation between system specifications, and a “Marking”. It is applied to construct four sliding window protocols that provide reliable data transfer over unreliable communication channels. The protocols use modulo-N sequence numbers. The first protocol is for channels that can only lose messages in transit. By refining this protocol, we obtain three protocols for channels that can lose, reorder, and duplicate messages in transit. The protocols herein are less restrictive and easier to implement than sliding window protocols previously studied in the protocol verification literature.

REFERENCES

• 1: ABADI, M., AND LAMPORT, L. The existence of refinement mappings. Tech. Rep. 29, Digital Systems Research Center, Palo Alto, Calif., Aug. 1988.
• 2: R. J. R. Back , R. Kurki-Suonio, Decentralization of process nets with centralized control, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.131-142, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806716]
• 3: R. J. R. Back , F. Kurki-Suonio, Distributed cooperation with action systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.4, p.513-554, Oct. 1988 [doi>10.1145/48022.48023]
• 4: Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, Proceedings of the eighth ACM symposium on Operating systems principles, p.1-11, December 14-16, 1981, Pacific Grove, California, United States
• 5: Mani Chandy , Jayadev Misra, An example of stepwise refinement of distributed programs: quiescence detection, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.326-343, July 1986 [doi>10.1145/5956.5958]
• 6: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 7: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 8: DIJKSTRA, E.W. The distribution snapshot of K. M. Chandy and L. Lamport. Tech. Rep. EWD-864, Univ. of Texas at Austin, Nov. 1983.
• 9: DIJKSTRA, E. W. Derivation of a termination detection algorithm for distributed computations. Tech. Rep. EWD-840, Umv. of Texas at Austin.
• 10: DIJKSTRA, E. W., AND SC~OLTEN C. S. Termination detection for diffusing computations. Inf. Process Lett. 11, I (Aug. 1980), 1-4.
• 11: Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978 [doi>10.1145/359642.359655]
• 12: HAILPERN, B. T., AND OWICKI, S. S Modular verificatlon of computer communication
• 13: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 14: F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
• 15: KNUTH, D.E. Verification of }ink-level protocols. BIT 21 (1981), 31-36.
• 16: Ron Koymans , R. K. Shyamasundar , Willem P. de Roever , Rob Gerth , S. Arun-Kumar, Compositional Semantics for Real-time Distributed Computing, Proceedings of the Conference on Logic of Programs, p.167-189, June 17-19, 1985
• 17: LAM, S. S., AND SHANKAR, A U. Protocol verification via projections. IEEE Trans. Softw. Eng. SE-IO, 4 (July 1984), 325-342.
• 18: Simon S. Lam , A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.755-775, July 1990 [doi>10.1109/32.56101]
• 19: Simon S. Lam , A. Udaya Shankar, Specifying modules to satisfy interfaces: a state transition system approach, University of Maryland at College Park, College Park, MD, 1988
• 20: Simon S. Lam , A. Udaya Shankar, A Composition Theorem for Layered Systems, Proceedings of the IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XI, p.93-108, June 18-20, 1991
• 21: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 22: Leslie Lamport, What it means for a concurrent program to satisfy a specification: why no one has specified priority, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.78-83, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318616]
• 23: Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989 [doi>10.1145/63238.63240]
• 24: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 25: 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]
• 26: Sandra Lynn Murphy, Service specification and protocol construction for a layered architecture, University of Maryland at College Park, College Park, MD, 1990
• 27: 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
• 28: OwIcKI, S., AND GRms, D. An axiomatic proof technique for parallel programs I. Acta Inf. 6, (1976), 319-340.
• 29: POSTEL, J., ED. Transmission control protocoh DARPA internet program protocol specification. RFC 793, Network Information Center, SRI International, 1981.
• 30: SASNANI, K. An algorithmic procedure for protocol verification. IEEE Trans. Commun. 36, 8 (Aug. 1988).
• 31: A. Udaya Shankar, Verified data transfer protocols with variable flow control, ACM Transactions on Computer Systems (TOCS), v.7 n.3, p.281-316, Aug. 1989 [doi>10.1145/65000.65003]
• 32: A. Udaya Shankar, Modular design principles for protocols with an application to the transport layer, University of Maryland at College Park, College Park, MD, 1990
• 33: A. Udaya Shankar , Simon S. Lam, An HDLC protocol specification and its verification using image protocols, ACM Transactions on Computer Systems (TOCS), v.1 n.4, p.331-368, Nov. 1983 [doi>10.1145/357377.357384]
• 34: SHANKAR, A. U., SND LAM, S.S. Time-dependent communication protocols. In Principles of Communication and Networking Protocols, S. S. Lam, Ed., IEEE Computer Soc~ety, New York, 1984.
• 35: S~ANKAn, A. U., AND LAM, S. S. Time-dependent distributed systems: proving safety, liveness and real-time properties. Distrib. Comput 2, 2 (1987), 61-79.
• 36: STENNING, N.V. A data transfer protocol. Comput. Networks I (Sept. 1976), 99-110.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Verification

Keywords:
assertional reasoning, conditional refinement, cyclic sequence numbers, interfaces, message lifetimes, sliding window protocols, stepwise refinement