Compositional verification of real-time systems with explicit clock temporal logic

P. Zhou, J.J.M. Hooman, R. Kuiper

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
4 Downloads (Pure)


To specify and verify real-time systems, we consider a real-time version of temporal logic called Explicit Clock Temporal Logic. Timing properties are specified by extending the classical framework of temporal logic with a special variable which explicitly refers to a global notion of time. Programs are written in an Occam-like real-time language with synchronous message passing. To show that a program satisfies a specification, we formulate a proof system which is proved to be sound and relatively complete. The proof system is compositional, which makes it possible to decompose the design of a large system into the design of subsystems. This is shown by the verification of a small part of an avionics system.
Original languageEnglish
Pages (from-to)294-323
JournalFormal Aspects of Computing
Issue number3
Publication statusPublished - 1996


Dive into the research topics of 'Compositional verification of real-time systems with explicit clock temporal logic'. Together they form a unique fingerprint.

Cite this