Skip to main content
SpringerLink
Log in

Putting time into proof outlines

  • Conference paper
  • First Online:
Real-Time: Theory in Practice (REX 1991)

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

Abstract

A logic for reasoning about timing properties of concurrent programs is presented. The logic is based on proof outlines and can handle maximal parallelism as well as resourceconstrained execution environments. The correctness proof for a mutual exclusion protocol that uses execution timings in a subtle way illustrates the logic in action.

Supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under Grant No. CCR-8701103, DARPA/NSF Grant No. CCR-9014363, and a grant from IBM Endicott Programming Laboratory.

Supported in part by NSF grant CCR-9003441.

Supported in part by Defense Advanced Research Projects Agency (DoD) under NASA Ames grant number NAG 2–593, and by grants from IBM and Siemens.

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. Dijkstra, E.W. Guarded commands, nondeterminacy and formal derivation of programs. CACM 18, 8 (Aug. 1975), 453–457.

    Google Scholar 

  2. Gries, D., and G. Levin. Assignment and procedure call proof rales. ACM TOPLAS 2, 4 (Oct. 1980), 564–579.

    Article  Google Scholar 

  3. Haase, V. Real-time Behavior of Programs. IEEE Transactions on Software Engineering SE-7, 5 (Sept. 1981), 494–501.

    Google Scholar 

  4. Hoare, C.A.R. An axiomatic basis for computer programming. CACM 12, 10 (Oct. 1969), 576–580.

    Google Scholar 

  5. Hooman, J. Specification and Compositional Verification of Real-time Systems. Ph.D. Thesis, Technische Universiteit Eindhoven. May 1991.

    Google Scholar 

  6. Lamport, L. A fast mutual exclusion algorithm. ACM TOCS 5, 1 (Feb. 1987), 1–11.

    Article  Google Scholar 

  7. Owicki, S.S., and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica 6, (1976), 319–340.

    Article  Google Scholar 

  8. Owicki, S.S., and L. Lamport. Proving liveness properties of concurrent programs. ACM TOPLAS 4, 3 (My 1982), 455–495.

    Article  Google Scholar 

  9. Schneider, F.B. On concurrent programming. In preparation.

    Google Scholar 

  10. Shaw, A. Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering SE-15, 7 (July 1989), 875–899.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853, Ithaca, New York

    Fred B. Schneider, Bard Bloom & Keith Marzullo

Authors
  1. Fred B. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bard Bloom
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Keith Marzullo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker C. Huizing W. P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schneider, F.B., Bloom, B., Marzullo, K. (1992). Putting time into proof outlines. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032010

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55564-3

  • Online ISBN: 978-3-540-47218-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation