## Temporal Proof Methodologies for Timed Transition Systems

Thomas A. Henzinger,
Zohar Manna, and Amir Pnueli

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. The
abstract notion of timed transition systems generalizes traditional
transition systems conservatively: qualitative fairness requirements
are replaced (and superseded) by quantitative lower-bound and
upper-bound timing constraints on transitions. This framework can
model real-time systems that communicate either through shared
variables or by message passing and real-time issues such as timeouts,
process priorities (interrupts), and process scheduling.

We exhibit two styles for the specification of real-time systems.
While the first approach uses time-bounded versions of the temporal
operators, the second approach allows explicit references to time
through a special clock variable. Corresponding to the two styles of
specification, we present and compare two different proof
methodologies for the verification of timing requirements that are
expressed in these styles. For the "bounded-operator" style, we
provide a set of proof rules for establishing bounded-invariance and
bounded-response properties of timed transition systems. This
approach generalizes the standard temporal proof rules for verifying
invariance and response properties conservatively. For the
"explicit-clock" style, we exploit the observation that every
time-bounded property is a safety property and use the standard
temporal proof rules for establishing safety properties.

*Information and Computation* 112:273-337, 1994.
Preliminary reports on this work appeared in
T.A. Henzinger, Z. Manna, and A. Pnueli,
"Temporal proof methodologies for real-time systems,"
*Proceedings of the
18th Annual Symposium on Principles of Programming Languages*
(POPL), ACM Press, 1991, pp. 353-366, and in
T.A. Henzinger, Z. Manna, and A. Pnueli,
"Timed transition systems,"
in
*Real Time: Theory in Practice*,
Lecture Notes in Computer Science 600,
Springer, 1992, pp. 226-251.

Download inofficial, sometimes updated
Postscript /
PDF document.
© 1991 ACM,
1992 Springer,
1994 Academic Press.