Skip to main content
SpringerLink
Log in

Composing specifications

  • Invited Lecture
  • Conference paper
  • First Online:
Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness (REX 1989)

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

Abstract

A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle if a component need behave correctly only when its environment does, since each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.

    Google Scholar 

  2. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Research Report 29, Digital Systems Research Center, 1988. To appear in Theoretical Computer Science. A preliminary version appeared in Proceedings of the Third Annual Symposium on Logic In Computer Science, pages 165–177, Edinburgh, Scotland, July 1988, IEEE Computer Society.

    Google Scholar 

  3. Martín Abadi, Leslie Lamport, and Pierre Wolper. Realizable and unrealizable program specifications. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, Lecture Notes in Computer Science, 372, pages 1–17. Springer-Verlag, July 1989.

    Google Scholar 

  4. Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, October 1985.

    MathSciNet  Google Scholar 

  5. Howard Barringer, Ruurd Kuiper, and Amir Pnueli. A really abstract concurrent model and its temporal logic. In Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 173–183. ACM, January 1986.

    Google Scholar 

  6. Morton Davis. Infinite games of perfect information. In M. Dresher, L. S. Shapley, and A. W. Tucker, editors, Advances in game theory, volume 52 of Annals of Mathematics Studies, pages 85–101. Princeton University Press, Princeton, New Jersey, 1964.

    Google Scholar 

  7. David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. PhD thesis, Carnegie Mellon University, February 1988.

    Google Scholar 

  8. C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281, 1972.

    Article  Google Scholar 

  9. C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, London, 1985.

    Google Scholar 

  10. Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, April 1983.

    Article  Google Scholar 

  11. Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657–668, Paris, September 1983. IFIP, North Holland.

    Google Scholar 

  12. Leslie Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1):32–45, January 1989.

    Google Scholar 

  13. S. S. Lam and A. U. Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, SE-10(4):325–342, July 1984.

    Google Scholar 

  14. Leslie Lamport and Fred B. Schneider. The “Hoare logic” of CSP, and all that. ACM Transactions on Programming Languages and Systems, 6(2):281–296, April 1984.

    Google Scholar 

  15. Nancy Lynch and Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Symposium on the Principles of Distributed Computing, pages 137–151. ACM, August 1987.

    Google Scholar 

  16. Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417–426, July 1981.

    Google Scholar 

  17. R. Milner. A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

    Google Scholar 

  18. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. Technical Report STAN-CS-87-1186, Department of Computer Science, Stanford University, October 1987.

    Google Scholar 

  19. Susan Owicki and David Gries. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 19(5):279–284, May 1976.

    Google Scholar 

  20. Susan Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.

    Article  Google Scholar 

  21. Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Krzysztof R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI Series, pages 123–144. Springer-Verlag, October 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Digital Equipment Corporation, 130 Lytton Avenue, 94301, Palo Alto, California, USA

    Martín Abadi & Leslie Lamport

Authors
  1. Martín Abadi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Leslie Lamport
    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

Abadi, M., Lamport, L. (1990). Composing 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_59

Download citation

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

  • 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