A compositional proof system for real-time systems based on explicit clock temporal logic : soundness and completeness
Ping Zhou, Jjm Jozef Hooman, Ruurd Kuiper · TU/e Research Portal · 1991
To specify and verify real-time systems, we consider a real-time version of temporal logic which is called Explicit Clock Temporal Logic. Timing properties are specified by simply ext.ending 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 in which concurrent processes communicate by synchronous message passing along channels. A proof system is provided to formally verify that a program satisfies a specification expressed in this logic. The proof system is compositional, that is, the verification of a complex statement can be done on the basis of the verifications of its components, without knowing the implementation of them. This allows splitting the verification of large systems into the verification of subsystems. The proof system is shown to be sound and relatively complete.