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 a real-time transition system is defined as a conservative extension of tranditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound real-time requirements for transitions.
We exhibit two styles for the specification of real-time properties. The first approach uses bounded versions of the temporal operators, while the second approach allows explicit references to the current time through a special clock variable. Corresponding to the two styles of specification, we present and compare two very different proof methodologies for the verification of real-time properties that are expressed in these styles.