Skip to main content
SpringerLink
Log in

An abstract account of composition

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1995 (MFCS 1995)

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

Abstract

We present a logic of specifications of reactive systems. The logic is independent of particular computational models, but it captures common patterns of reasoning with assumption-commitment specifications. We use the logic for deriving proof rules for TLA and CTL* specifications.

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. Martín Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.

    Google Scholar 

  2. Martín Abadi and Leslie Lamport. Conjoining specifications. Research Report 118, Digital Equipment Corporation, Systems Research Center, 1993. To appear in ACM Transactions on Programming Languages and Systems.

    Google Scholar 

  3. Martín Abadi and Stephan Merz. On TLA as a logic. In Manfred Broy, editor, Deductive Program Design, NATO ASI Series. Springer-Verlag, Berlin, 1995. To appear.

    Google Scholar 

  4. Martín Abadi and Gordon Plotkin. A logical view of composition and refinement. In Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 323–332. ACM, January 1991.

    Google Scholar 

  5. Martín Abadi and Gordon Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, June 1993.

    Google Scholar 

  6. Manfred Broy. A functional rephrasing of the assumption/commitment specification style. SFB-Bericht 342/10/94, TUM-I9417, Techn. Univ. München, Munich, April 1994.

    Google Scholar 

  7. Antonio Cau and Pierre Collette. Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency. Acta Informatica, 1995. To appear.

    Google Scholar 

  8. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of theoretical computer science, pages 997–1071. Elsevier Science Publishers B.V., 1990.

    Google Scholar 

  9. Orna Grumberg and David E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, May 1994.

    Google Scholar 

  10. Alfred Horn. Logic with truth values in a linearly ordered Heyting algebra. Journal of Symbolic Logic, 34(3):395–408, September 1969.

    Google Scholar 

  11. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, October 1983.

    Article  Google Scholar 

  12. Bengt Jonsson and Yih-Kuen Tsay. Assumption/guarantee specifications in lineartime temporal logic. In Proceedings of TAPSOFT '95, Lecture Notes in Computer Science, Berlin, May 1995. Springer-Verlag.

    Google Scholar 

  13. Bernhard Josko. Verifying the correctness of AADL modules using model checking. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 386–400. Springer-Verlag, Berlin, 1989.

    Google Scholar 

  14. Bernhard Josko. Modular specification and verification of reactive systems. Habilitationsschrift, Univ. Oldenburg, Fachbereich Informatik, April 1993.

    Google Scholar 

  15. 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 

  16. Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Google Scholar 

  17. Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Trans. Software Engineering, 7(4):417–426, July 1981.

    Google Scholar 

  18. 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 

  19. Ketil StØlen, Frank Dederichs, and Rainer Weber. Assumption/commitment rules for networks of asynchronously communicating agents. SFB-Bericht 342/2/93, TUM-I9303, Techn. Univ. München, Munich, February 1993.

    Google Scholar 

  20. A. S. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction, volume 1. North Holland, Amsterdam, 1988.

    Google Scholar 

  21. Moshe Vardi. On the complexity of modular model checking. In Proceedings of the Tenth Symposium on Logic in Computer Science. IEEE, June 1995.

    Google Scholar 

  22. Qiwen Xu, Antonio Cau, and Pierre Collette. On unifying assumption-commitment style proof rules for concurrency. In Bengt Jonsson and Joachim Parrow, editors, Proceedings of the Fifth International Conference on Concurrency Theory (CONCUR '94), volume 836 of Lecture Notes in Computer Science, pages 267–282, Berlin, 1994. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Systems Research Center, Digital Equipment Corporation, 130 Lytton Avenue, 94301, Palo Alto, CA, USA

    Martín Abadi

  2. Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290, München, Germany

    Stephan Merz

Authors
  1. Martín Abadi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jiří Wiedermann Petr Hájek

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abadi, M., Merz, S. (1995). An abstract account of composition. In: Wiedermann, J., Hájek, P. (eds) Mathematical Foundations of Computer Science 1995. MFCS 1995. Lecture Notes in Computer Science, vol 969. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60246-1_155

Download citation

  • DOI: https://doi.org/10.1007/3-540-60246-1_155

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60246-0

  • Online ISBN: 978-3-540-44768-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation