Report Number: CS-TR-91-1383
Institution: Stanford University, Department of Computer Science
Title: Temporal proof methodologies for real-time systems
Author: Henzinger, Thomas A.
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: September 1991
Abstract: 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 time-outs, process priorities (interrupts), and
process scheduling.
We exhibit two styles for the specification of real-time
systems. While the first approach uses bounded versions of
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 fundamentally different proof methodologies
for the verification of timing requirements that are
expressed in these styles. For the bounded-operatoT 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/91/1383/CS-TR-91-1383.pdf