Abstract
We present a heuristic to derive specifications of distributed systems by stepwise refinement. The heuristic is based upon a conditional refinement relation between specifications. 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. They are less restrictive and easier to implement than sliding window protocols previously studied in the protocol verification literature.
The work of A. Udaya Shankar was supported by National Science Foundation under grant no. ECS-8502113 and grant no. NCR-8904590. The work of Simon S. Lam was supported by National Science Foundation under grant no. NCR-8613338 and by a grant from the Texas Advanced Research Program. This paper is an abbreviated version of [18].
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R.J.R. Back and R. Kurki-Suonio, “Decentralization of process nets with a centralized control,” Second ACM SIGACT-SIGCOPS Symp. on Prin. of Distr. Comput., Montreal, Aug. 1983, pp. 131–142.
R.J.R. Back and R. Kurki-Suonio, “A case study in constructing distributed algorithms: Distributed exchange sort,” Proc. of Winter School on Theoretical Computer Science, Lammi, Finland, Jan. 1984, Finnish Soc. of Inf. Proc. Sc., pp. 1–33.
K.M. Chandy and J. Misra, “An example of stepwise refinement of distributed programs: Quiescence detection,” ACM Trans. on Prog. Lang. and Syst., Vol. 8, No. 3, July 1986, pp. 326–343.
K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, Reading, MA, 1988.
E.W. Dijkstra, A Discipline of Programming, Prentice-Hall, Englewood Cliffs, N.J., 1976.
E.W. Dijkstra, L. Lamport, A.J. Martin, C.S. Scholten, “On-the-fly garbage collection: An exercise in cooperation,” Commun. ACM, Vol. 21, No. 11, November 1978, pp. 966–975.
E.W. Dijkstra, C.S. Scholten, “Termination detection for diffusing computations,” Inform. Proc. Letters, Vol. 11, No. 1, August 1980, pp. 1–4.
E.W. Dijkstra, “Derivation of a termination detection algorithm for distributed computations,” Tech. Report, EWD-840.
E.W. Dijkstra, “The distributed snapshot of K.M. Chandy and L. Lamport,” Tech. Report, EWD-864, November 1983.
Transmission Control Protocol, DDN Protocol Handbook: DoD Military Standard Protocols, DDN Network Information Center, SRI, MILSTD 1778, Aug 1983.
D.E. Knuth, “Verification of link-level protocols,” BIT, Vol. 21, pp. 31–36, 1981.
S.S. Lam and A.U. Shankar, “Protocol verification via projections,” IEEE Trans. on Software Engineering, Vol. SE-10, No. 4, July 1984, pp. 325–342.
S.S. Lam and A.U. Shankar, “Specifying implementations to satisfy interfaces: A state transition system approach,” presented at the 26th Annual Lake Arrowhead Workshop on How will we specify concurrent systems in the year 2000?, September 1987; full version available as Technical Report TR-88-30, Department of Computer Sciences, University of Texas at Austin, August 1988 (revised June 1989).
S.S. Lam and A.U. Shankar, “A relational notation for state transition systems,” Technical Report TR-88-21, Department of Computer Sciences, University of Texas at Austin, May 1988 (revised August 1989); an abbreviated version appears in these proceedings of the REX Workshop on Refinement of Distributed Systems under the title “Refinement and projection of relational specifications.”
K. Sere, “Stepwise removal of virtual channels in distributed algorithms,” Second Int. Workshop on Dist. Alg., Amsterdam, 1987.
A.U. Shankar and S.S. Lam, “Time-dependent communication protocols,” Tutorial: Principles of Communication and Networking Protocols, S. S. Lam (ed.), IEEE Computer Society, 1984.
A.U. Shankar and S.S. Lam, “Time-dependent distributed systems: proving safety, liveness and real-time properties,” Distributed Computing, Vol. 2, No. 2, pp. 61–79, 1987.
A.U. Shankar and S.S. Lam, “A stepwise refinement heuristic for protocol construction,” Technical Report CS-TR-1812, Department of Computer Science, University of Maryland, March 1987 (revised March 1989).
A.U. Shankar, “Verified data transfer protocols with variable flow control,” ACM Transactions on Computer Systems, Vol. 7, No. 3, August 1989; an abbreviated version appears in Proc. ACM SIGCOMM '86 Symposium, Aug 1986, under the title “A verified sliding window protocol with variable flow control.”
N.V. Stenning, “A data transfer protocol,” Computer Networks, Vol. 1, pp. 99–110, September 1976.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shankar, A.U., Lam, S.S. (1990). Construction of network protocols by stepwise refinement. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_83
Download citation
DOI: https://doi.org/10.1007/3-540-52559-9_83
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52559-2
Online ISBN: 978-3-540-47035-9
eBook Packages: Springer Book Archive