skip to main content
10.5555/952786.952803acmconferencesArticle/Chapter ViewAbstractPublication PagesiwssdConference Proceedingsconference-collections
Article
Free access

A compositional proof system for real-time systems based on explicit clock temporal logic

Published: 25 October 1991 Publication History

Abstract

To specify timing properties of real-time systems, we consider Explicit Clock Temporal Logic. Programs are written in an Occam-like real-time language. A proof system is provided to formally verify that a program satisfies a specification expressed in our real-time version of temporal logic. The proof system is compositional, sound, and relatively complete.

References

[1]
H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Proc. ACM Symp. on Theory of Computing, pages 51--63, 1984.
[2]
E. Emerson, A. Mok, A. Sistla, and J. Srinivasan. Quantitative temporal reasoning. presented at Workshop On Automatic Verification Methods For Finite State Systems, Grenoble, 1989.
[3]
E. Harel. Temporal analysis of real-time systems. Master's thesis, The Weizmann Institute of Science, Rehovot, Israel, 1988.
[4]
E. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. In Proc. Symp. Logic in Computer Science, pages 402--413, 1990.
[5]
J. Hooman. A denotational real-time semantics for shared processors. In Parallel Architectures and Languages Europe, volume II, pages 184--201. LNCS 506, Springer-Verlag, 1991.
[6]
J. Hooman. Specification and Compositional Verification of Real-Time Systems. PhD thesis, Eindhoven University of Technology, 1991.
[7]
J. Hooman and J. Widom. A temporal-logic based compositional proof system for real-time message passing. In Parallel Architectures and Languages Europe, volume II, pages 424--441. LNCS 366, Springer-Verlag, 1989.
[8]
INMOS Limited. OCCAM 2 Reference Manual, 1988.
[9]
R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255--299, 1990.
[10]
Z. Manna and A. Pnueli. Verification of concurrent programs: a temporal proof system. In Foundations of Computer Science IV, Distributed Systems: Part 2, volume 159 of Mathematical Centre Tracts, pages 163--255, 1982.
[11]
J. Ostroff. Temporal Logic for Real-Time Systems. Advanced Software Development Series. Research Studies Press, 1989.
[12]
A. Pnueli. The temporal logic of programs. In Proc. of the 18th Symposium on Foundations of Computer Science, pages 46--57, 1977.
[13]
P. Zhou, J. Hooman, and R. Kuiper. A compositional proof system for real-time systems based on explicit clock temporal logic: soundness and completeness. Technical report, Eindhoven University of Technology, 1991.
  1. A compositional proof system for real-time systems based on explicit clock temporal logic

        Recommendations

        Comments

        Information & Contributors

        Information

        Published In

        IWSSD '91: Proceedings of the 6th international workshop on Software specification and design
        October 1991
        257 pages
        ISBN:0818623209

        Sponsors

        Publisher

        IEEE Computer Society Press

        Washington, DC, United States

        Publication History

        Published: 25 October 1991

        Check for updates

        Qualifiers

        • Article

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • 0
          Total Citations
        • 87
          Total Downloads
        • Downloads (Last 12 months)3
        • Downloads (Last 6 weeks)1
        Reflects downloads up to 21 Dec 2024

        Other Metrics

        Citations

        View Options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Login options

        Media

        Figures

        Other

        Tables

        Share

        Share

        Share this Publication link

        Share on social media