An interleaving model for real-time

Abstract

Real-time is incorporated into the interleaving model, which is used for the practical specification and verification of many properties of concurrent systems, 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. Proof rules are presented and used 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 termination of shared-variables multiprocessing systems whose semantics is defined in terms of real-time transition systems.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>