Skip to main content
SpringerLink
Log in
Book cover

Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems)

REX 1989: Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness pp 454–486Cite as

Refinement and projection of relational specifications

  • Technical Contributions
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 430))

Abstract

A relational specification consists of a state transition system and a set of fairness assumptions. The state transition system is specified using two basic constructs: state formulas that respresent sets of states, and event formulas that represent sets of state transitions. We present a theory of refinement of relational specifications. Several refinement relations between specifications are defined. To illustrate our concepts and methods, three specifications of the alternating-bit protocol are given. We also apply the theory to explain “auxiliary variables.” Other applications of the theory to protocol verification, composition, and conversion are discussed. Our approach is compared with the approaches of other authors.

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. The work of A. Udaya Shankar was supported by National Science Foundation under grant no. ECS-8502113 and grant no. NCR-8904590. This paper is an abbreviated version of [Lam & Shankar 88].

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport, “The Existence of Refinement Mappings,” Technical Report, Digital Systems Research Center, Palo Alto, California, August 1988.

    Google Scholar 

  2. K. L. Calvert and S. S. Lam, “Formal Methods for Protocol Conversion,” to appear in IEEE Journal on Selected Areas in Communications, January 1990.

    Google Scholar 

  3. K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, Reading, MA, 1988.

    Google Scholar 

  4. B.T. Hailpern and S. Owicki, “Modular Verification of Computer Communication Protocols,” IEEE Transactions on Communications, Vol. COM-31, No. 1, January 1983.

    Google Scholar 

  5. E.C.R Hehner, “Predicative Programming, Part I and Part II,” Communications of the ACM, Vol. 27, No. 2, February 1984.

    Google Scholar 

  6. IBM Corporation, Systems Network Architecture Format and Protocol Reference Manual: Architecture Logic, IBM Form No. SC32-3112-2, 1980.

    Google Scholar 

  7. ISO/TC97/SC21/WG16-1 N422 Estelle — A Formal Description Technique Based on an Extended State Transition Model, February 1985.

    Google Scholar 

  8. S. S. Lam, “Protocol Conversion,” IEEE Transactions on Software Engineering, Vol. 14, No. 3, March 1988.

    Google Scholar 

  9. S. S. Lam and A. U. Shankar, “Protocol Verification via Projections,” IEEE Transactions on Software Engineering, Vol. SE-10, No. 4, July 1984.

    Google Scholar 

  10. S. S. Lam and A. U. Shankar, “Specifying Implementations to Satisfy Interfaces: A State Transition System Approach,” presented at the 26th 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).

    Google Scholar 

  11. S. S. Lam and A. U. Shankar, “A Relational Notation for State Transition Systems,” Technical Report TR-88-21, Department of Computer Sciences, The University of Texas at Austin, May 1988 (Second Revision, August 1989).

    Google Scholar 

  12. L. Lamport, “What Good is Temporal Logic?” Proceedings Information Processing 83, IFIP, 1983.

    Google Scholar 

  13. L. Lamport, “Specifying Concurrent Program Modules,” ACM TOPLAS, Vol. 5, No. 2, April 1983.

    Google Scholar 

  14. L. Lamport, “What it means for a concurrent program to satisfy a specification: Why no one has specified priority,” Proceedings of the 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985.

    Google Scholar 

  15. N.A. Lynch and M.R. Tuttle, “Hierarchical Correctness Proofs for Distributed Algorithms,” Proceedings of the ACM Symposium on Principles of Distributed Computing, Vancouver, B.C., August 1987.

    Google Scholar 

  16. Z. Manna and A. Pnueli, “Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs,” Science of Computer Programming, Vol. 4, 1984.

    Google Scholar 

  17. Z. Manna and R. Waldinger, The Logical Basis for Computer Programming, Addison-Wesley, Reading, MA, 1985.

    Google Scholar 

  18. S.L. Murphy and A.U. Shankar, “A Verified Connection Management Protocol for the Transport Layer,” Proceedings ACM SIGCOMM '87 Workshop, Stowe, Vermont, August 1987.

    Google Scholar 

  19. S.L. Murphy and A.U. Shankar, “Service Specification and Protocol Construction for the Transport Layer,” Proceedings ACM SIGCOMM '88 Symposium, Stanford University, August 1988.

    Google Scholar 

  20. S. Owicki and D. Gries, “Verifying Properties of Parallel Programs: An Axiomatic Approach,” Communications of the ACM, Vol. 19, No. 5, May 1976.

    Google Scholar 

  21. S. Owicki and L. Lamport, “Proving Liveness Properties of Concurrent Systems,” ACM TOPLAS, Vol. 4, No. 3, 1982.

    Google Scholar 

  22. T. F. Piatkowski, “The State of The Art in Protocol Engineering,” Proceedings ACM Sigcomm '86 Symposium, Stowe, Vermont, 1986.

    Google Scholar 

  23. A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends,” in Current Trends in Concurrency: Overviews and Tutorials, J.W, deBakker et al. (ed.), LNCS 224, Springer Verlag, 1986.

    Google Scholar 

  24. K. Sabnani, “An Algorithmic Procedure for Protocol Verification,” IEEE Transactions on Communications, Vol. 36, No. 8, August 1988.

    Google Scholar 

  25. J. Scheid and S. Holtsberg, Ina Jo Specification Language Reference Manual, System Development Group, Unisys Corp., Santa Monica, CA, September 1988.

    Google Scholar 

  26. 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 Proceedings ACM SIGCOMM '86, Stowe, Vermont, August 1986.

    Google Scholar 

  27. A.U. Shankar and S.S. Lam, “An HDLC Protocol Specification and its Verification Using Image Protocols,” ACM TOCS, Vol. 1, No. 4, November 1983.

    Google Scholar 

  28. A.U. Shankar and S.S. Lam, “Time-dependent communication protocols,” in Tutorial: Principles of Communication and Networking Protocols, S.S. Lam (ed.), IEEE Computer Society, 1984.

    Google Scholar 

  29. A.U. Shankar and S.S. Lam, “Time-dependent distributed systems: proving safety, liveness, and real-time properties,” Distributed Computing, Vol. 2, No. 2, 1987.

    Google Scholar 

  30. 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).

    Google Scholar 

  31. C.H. West, “A General Technique for Communications Protocol Validation,” IBM Journal of Research and Development, Vol. 22, July 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Sciences, The University of Texas at Austin, 78712, Austin, Texas

    Simon S. Lam

  2. Department of Computer Science and Institute for Advanced Computer Studies, University of Maryland, 20742, College Park, Maryland

    A. Udaya Shankar

Authors
  1. Simon S. Lam
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Udaya Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lam, S.S., Shankar, A.U. (1990). Refinement and projection of relational specifications. 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_75

Download citation

  • DOI: https://doi.org/10.1007/3-540-52559-9_75

  • 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

Publish with us

Policies and ethics

Search

Navigation