Compositional verification of real-time systems using extended Hoare triples

  • Jozef Hooman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


To specify and verify the real-time behaviour of programs, a formalism based on Hoare triples (precondition, program, postcondition) is introduced. Programs are written in an Occam-like programming language with synchronous message passing along unidirectional channels. Real-time is incorporated by delaystatements and time-outs. To deal with reactive systems, a Hoare triple is extended with a third assertion, called commitment, which expresses the real-time communication interface of the program. We formulate a compositional axiomatization for these extended Hoare triples, first using the maximal parallelism assumption which represents the situation in which each process has its own processor. Next this framework is generalized to multiprogramming where several processes may share a single processor and scheduling is based on priorities of statements.


Real-time Specification Verification Compositionality Hoare triples 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [GL90]
    R. Gerber and I. Lee. CCSR: a calculus for communicating shared resources. In CONCUR '90, pages 263–277. LNCS 458, Springer-Verlag, 1990.Google Scholar
  2. [Haa81]
    V.H. Haase. Real-time behaviour of programs. IEEE Transactions on Software Engineering, SE-7(5):494–501, 1981.Google Scholar
  3. [HLP90]
    E. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. In Proceedings Symposium on Logic in Computer Science, pages 402–413, 1990.Google Scholar
  4. [HMP91]
    T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time systems. In Proceedings 18th ACM Symposium on Principles of Programming Languages, pages 353–366, 1991.Google Scholar
  5. [Hoa69]
    C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 583, 1969.CrossRefGoogle Scholar
  6. [Hoo91a]
    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.Google Scholar
  7. [Hoo91b]
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.Google Scholar
  8. [Koy90]
    R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255–299, 1990.CrossRefGoogle Scholar
  9. [MP82]
    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.Google Scholar
  10. [Occ88a]
    INMOS Limited. Communicating process architecture, 1988.Google Scholar
  11. [Occ88b]
    INMOS Limited. OCCAM 2 Reference Manual, 1988.Google Scholar
  12. [Ost89]
    J. Ostroff. Temporal Logic for Real-Time Systems. Advanced Software Development Series. Research Studies Press, 1989.Google Scholar
  13. [SBM92]
    F. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In REX Workshop on Real-Time: Theory in Practice. LNCS (this volume), Springer-Verlag, 1992.Google Scholar
  14. [Zwi89]
    J. Zwiers. Compositionality, Concurrency and Partial Correctness. LNCS 321, Springer-Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Jozef Hooman
    • 1
  1. 1.Dept. of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations