We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.
Appeared in4th International AMAST Workshop on Real-time Systems,
LNCS vol 1231, Springer-Verlag, pp 22-43, 1997.
An extended
version of this paper appeared in
Theoretical Computer Science, Vol. 253, pp 27-60, 2001.
Postscript, PDF. © 1997, Springer Verlag.