An interleaving model for real-time

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