Specification and Compositional Verification of Real-Time Systems

The research described in this monograph concerns the formal
specification   and compositional verification of real-time
systems. A real-time programminglanguage is considered in
which concurrent processes communicate by            synchronous
message passing along unidirectional channels. To                     specifiy
functional and timing properties of programs, two                           formalisms
are investigated: one using a real-time version of                     temporal
logic, called Metric Temporal Logic, and another which is
basedon extended Hoare triples. Metric Temporal Logic
provides a concise notationto express timing properties and
to axiomatize the programming language,      whereas Hoare-style
formulae are especially convenient for the verification of
sequential constructs. For both approaches a compositional
proof      system has been formulated to verify that a program
satisfies a                  specification. To deduce timing properties of
programs, first maximal         parallelism is assumed, modeling the
situation in which each process has itsown processor. Next,
this model is generalized to multiprogramming where      several
processes may share a processor and scheduling is based                  on
priorities. The proof systems are shown to be sound and
relatively   complete with respect to a denotational semantics
of the programming            language. The theory is illustrated by an
example of a watchdog timer.