Temporal Proof Methodologies for Real-Time Systems,
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The authors extend the specification language of temporal logic, the corresponding verification framework, and the underling 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. The authors 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 two styles of specification the authors present and compare two fundamentally different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, the authors 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 clockstyle the authors exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties.
- Computer Programming and Software