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.