TEMPORAL PROOF METHODOLOGIES FOR TIMED TRANSITION-SYSTEMS

We extend the specification language of temporal logic, the correspond ing verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract noti on of timed transition systems generalizes traditional transition syst ems conservatively: qualitative fairness requirements are replaced (an d superseded) by quantitative lower-bound and upper-bound timing const raints 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 timeouts, process priorities (interrupts), a nd process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit refere nces to time through a special clock variable. Corresponding to the tw o styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are exp ressed in these styles. For the bounded-operator style, we provide a s et of proof rules for establishing bounded-invariance and bounded-resp once properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and respon se properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety pro perties. (C) 1994 Academic Press, Inc.