Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computer Aided Systems Theory

EUROCAST 1997: Computer Aided Systems Theory — EUROCAST'97 pp 123–145Cite as

A dense-time temporal logic with nice compositionality properties

  • 2 Theory and Methods
  • Conference paper
  • First Online:

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

Abstract

A dense temporal logic specification method for the development of reactive systems is introduced. The two development constructs of this method are refinement and composition. A reactive system is specified by a pair consisting of a machine and a condition on the computations of this machine. In order to compose such systems compositionally, each machine step contains additional information such as “this is a system step”, or “this is an environment step” or “this is a communication step”. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism.

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. P Aczel. On an inference rule for parallel composition, 1983. Unpublished, University of Manchester.

    Google Scholar 

  2. K. R. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2(4):226–241, 1988.

    Article  Google Scholar 

  3. M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.

    Article  Google Scholar 

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

    Article  Google Scholar 

  5. B. Alpern and F. Schneider. Proving boolean combinations of deterministic properties. In Proceedings of the second symposium on logic in computer science, pages 131–137. IEEE, June 1987.

    Google Scholar 

  6. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Proceedings of 16th ACM Symposium on Theory of Computing, pages 51–63, 1984.

    Google Scholar 

  7. H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal semantics. In Proc. 13th ACM Symp. Princ. of Prog. Lang., pages 173–183, 1986.

    Google Scholar 

  8. J.P. Burgess. Axioms for tense logic, i. “since” and “until”. Notre Dame Journal of Formal Logic, 23(4):367–374, October 1982.

    Google Scholar 

  9. J.P. Burgess. Basic tense logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic., volume II, pages 89–133. Reidel Publishers, 1984.

    Google Scholar 

  10. A. Cau. Compositional Verification and Specification of Refinement for Reactive Systems in Dense Time Temporal Logic. PhD thesis, Christian-Albrechts-Universität zu Kiel, 1995. Available as report no. 9601.

    Google Scholar 

  11. A. Cau and P. Collette. Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency. Acta Informatica, 33(2):153–176, 1996.

    Article  Google Scholar 

  12. E. Diepstraten and R. Kuiper. Abadi & Lamport and Stark: towards a proof theory for stuttering, dense domains and refinements mappings. In LNCS 430: Proc. of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, pages 208–238. Springer-Verlag, 1990.

    Google Scholar 

  13. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, London, 1984.

    Google Scholar 

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

    Article  Google Scholar 

  15. Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, LNCS 803: A Decade of Concurrency, Reflections and Perspectives, pages 273–346. Springer-Verlag, 1993.

    Google Scholar 

  16. L. Lamport. What good is temporal logic. In R.E.A. Manson, editor, Information Processing 83: Proc. of the IFIP 9th World Congress, pages 657–668. Elsevier Science Publishers, North Holland, 1983.

    Google Scholar 

  17. L. Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872–923, May 1994.

    Article  Google Scholar 

  18. J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417–426, July 1981.

    Google Scholar 

  19. Z. Manna and A. Pnueli. An exercise in the verification of multi-process programs. Technical report, Stanford University, 1989.

    Google Scholar 

  20. E.W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachusetts Inst. of Technology, 1984. Available as Report No. MIT/LCSfIR-342.

    Google Scholar 

  21. J. Zwiers, J. Coenen, and W.-P. de Roever. A note on compositional refinement. In C. B. Jones, R. C. Shaw, and T. Denvir, editors, 5th Refinement Workshop, Workshops in Computing, pages 342–366, London, January 1992. BCS-FACS, Springer Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Technology Research Laboratory, Department of Computer Science, De Montfort University, The Gateway, Leicester, LEI 913H, UK

    Antonio Cau

  2. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Preußerstr. 1-9, D-24105, Kiel, Germany

    Willem-Paul de Roever

Authors
  1. Antonio Cau
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Willem-Paul de Roever
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Franz Pichler Roberto Moreno-Díaz

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cau, A., de Roever, WP. (1997). A dense-time temporal logic with nice compositionality properties. In: Pichler, F., Moreno-Díaz, R. (eds) Computer Aided Systems Theory — EUROCAST'97. EUROCAST 1997. Lecture Notes in Computer Science, vol 1333. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0025039

Download citation

  • DOI: https://doi.org/10.1007/BFb0025039

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63811-7

  • Online ISBN: 978-3-540-69651-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation