Skip to main content
SpringerLink
Log in

Towards the hierarchical, temporal logic, specification of concurrent systems

  • 4. Solutions
  • Conference paper
  • First Online:
The Analysis of Concurrent Systems

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

Abstract

A hierarchical specification method is given which, through the use of a past time temporal logic, handles both safety and liveness requirements. The technique is applied to the specification of a "two way channel with disconnect", and in the partial development of a "packet switching communications network". An inference rule for the justification of parallel composition is indicated.

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. H.Barringer and R.Kuiper A Temporal Logic Specification Method Supporting Hierarchical Development Extended Abstract Dept. of Computer Science, University of Manchester. Nov. 1983

    Google Scholar 

  2. C.B. Jones Specification and Design of (Parallel) Programs Proc. IFIP 83, Paris, North Holland, 1983.

    Google Scholar 

  3. Z. Manna and A. Pnueli Verification of Concurrent Programs: The Temporal Framework in "The Correctness Problem in Computer Science" ed. R.S. Boyer and J.S. Moore International Lecture Series in Computer Science, pp215–273, Academic Press, London, 1982.

    Google Scholar 

  4. Z.Manna and A.Pnueli Verification of Concurrent Programs: A Temporal Proof System Computer Science Report, Stanford University, 1983.

    Google Scholar 

  5. S.S. Owicki and L. Lamport Proving Liveness Properties of Concurrent Programs ACM TOPLAS, Vol. 4, No. 3, pp455–495, July 1982.

    Google Scholar 

  6. A. Pnueli The Temporal Semantics of Concurrent Computation in Proc. of the Symp. on Semantics of Concurrent Computation, Evian, France, July 1979 Springer-Verlag LNCS, Vol. 70, pp1–20.

    Google Scholar 

  7. A.Prior Past, Present and Future Oxford University Press, 1967.

    Google Scholar 

  8. A.P.Sistla, E.M.Clarke, N.Francez and Y.Gurevich Can Buffers be Specified in Linear Temporal Logic? Proc. 1st ACM SIGACT/SIGOPS Conf. on PODC, Ottawa, Aug. 1982.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester

    Howard Barringer & Ruurd Kuiper

Authors
  1. Howard Barringer
    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

B. T. Denvir W. T. Harwood M. I. Jackson M. J. Wray

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barringer, H., Kuiper, R. (1985). Towards the hierarchical, temporal logic, specification of concurrent systems. In: Denvir, B.T., Harwood, W.T., Jackson, M.I., Wray, M.J. (eds) The Analysis of Concurrent Systems. Lecture Notes in Computer Science, vol 207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16047-7_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-16047-7_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16047-2

  • Online ISBN: 978-3-540-39731-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation