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 208–238Cite as

Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings

  • Technical Contributions
  • Conference paper
  • First Online:

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

Abstract

Crucial in proving refinement between specifications (of concurrent programs) is the role of ghost variables. On one hand they enhance expressivity. On the other hand they introduce stuttering and, in the case of refinement mappings, lead to the non-existence of such mappings.

Semantically, the these problems are solved satisfactorily in the work of Abadi & Lamport [AL88]. Syntactically, however, their solutions have no obvious prooftheoretic counterpart. By formulating Abadi & Lamport's concepts within Stark's formalism for dense Linear Time Temporal Logic [Sta88] a step in this direction is made.

(Extended Abstract)

Supported by the Netherlands Organisation for Scientific Research (NWO) under grant NF 62–519: Refinement and Education in Concurrent Systems (REX).

Supported partially by ESPRIT project no. 3096 “SPEC: Formal Methods and Tools for the Development of Distributed and Real Time Systems”.

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. In Third annual symposium on Logic in Computer Science, pages 165–175. IEEE, July 1988.

    Google Scholar 

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

    MathSciNet  Google Scholar 

  3. H. Barringer, R. Kuiper, and A. Pnueli. A really abstract concurrent model and its temporal logic. In 13th Annual ACM Symposium on Principles of Programming Languages, pages 173–183, 1986.

    Google Scholar 

  4. E.C.M. Diepstraten. Specifying observable behavior using temporal logic and auxiliary variables. Master's thesis, Eindhoven University of Technology, July 1989.

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  7. L. Lamport. An axiomatic semantics of concurrent programming languages. In K.R. Apt, editor, NATO ASI Series, vol. F13: Logics and Models of Concurrent Systems, pages 77–122. Springer-Verlag, January 1985.

    Google Scholar 

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

    Google Scholar 

  9. Z. Manna and A. Pnueli. Verification of concurrent programs: The temporal framework. In Acadeic Press, editor, The Correctness Problem in Computer Science, chapter 5, pages 215–273. International Lecture Series in Computer Science, London, 1982.

    Google Scholar 

  10. E.W. Stark. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135–154, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Eduard Diepstraten & Ruurd Kuiper

Authors
  1. Eduard Diepstraten
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ruurd Kuiper
    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

Diepstraten, E., Kuiper, R. (1990). Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings. 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_66

Download citation

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

  • 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