The Temporal Specification and Verification of Real-Time Systems
Thomas A. Henzinger
We extend the specification language of temporal logic, the corresponding
verification framework, and the underlying computational model to deal with
real-time properties of reactive systems.
We introduce the abstract computational model of timed transition
systems as a conservative extension of traditional transition systems:
qualitative fairness requirements are superseded by quantitative real-time
constraints on the transitions.
Digital clocks are introduced as observers of continuous real-time
We justify our semantical abstractions by demonstrating that a wide variety
of concrete real-time systems can be modeled adequately.
We present two conservative extensions of temporal logic that allow for the
specification of timing constraints:
while timed temporal logic provides access to time through a novel
kind of time quantifier, metric temporal logic refers to time
through time-bounded versions of the temporal operators.
We justify our choice of specification languages by developing a general
framework for the classification of real-time logics according to their
complexity and expressive power.
We develop tools for determining if a real-time system that is modeled as a
timed transition system meets a specification that is given in timed
temporal logic or in metric temporal logic.
We present both model-checking algorithms for the automatic
verification of finite-state real-time systems and proof methods for
the deductive verification of real-time systems.
Both techniques are conservative generalizations of the corresponding
conventional approaches to program verification, which abstract time from
Ph.D. Thesis, Technical Report STAN-CS-91-1380, Stanford University,
August 1991, 272 pages.