Deductive Verification of Real-time systems using STeP

Nikolaj Bjorner, Zohar Manna, Henny Sipma, Tomas Uribe

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. We also discuss global and modular proofs of the branching-time property of non-Zenoness. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.

In Theoretical Computer Science, Vol. 253, pp 27-60, 2001.

Postscript, PDF. © 2001, Elsevier Science B.V.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Fri Mar 30 08:26:19 PST 2001