Deductive verification of real-time systems using STeP

We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logi c. We show how deductive verification rules, verification diagrams, and aut omatic invariant generation can be used to establish properties of real-tim e systems in this framework. We also discuss global and modular proofs of t he branching-time property of non-Zenoness. As an example, we present the m echanical verification of the generalized railroad crossing case study usin g the Stanford Temporal Prover, STeP. (C) 2001 Elsevier Science B.V. All ri ghts reserved.