Report Number: CS-TR-90-1329
Institution: Stanford University, Department of Computer Science
Title: An interleaving model for real time.
Author: Henzinger, Thomas A.
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: September 1990
Abstract: The interleaving model is both adequate and sufficiently
abstract to allow for the practical specification and
verification of many properties of concurrent systems. We
incorporate real time into this model by defining the
abstract notion of a real-time transition system as a
conservative extension of traditional transition systems:
qualitative fairness requirements are replaced (and
superseded) by quantitative lower-bound and upper-bound
real-time requirements for transitions. We present proof
rules to establish lower and upper real-time bounds for
response properties of real-time transition systems. This
proof system can be used to verify bounded-invariance and
bounded-response properties, such as timely terrnination of
shared-variables multi-process systems, whose semantics is
defined in terms of real-time transition systems.