Computer Science Department, Stanford University Stanford, CA 94305

Appeared in * International Conference*
*on Computer Aided Verification*, pp.415-418.
vol. 1102 of Lecture Notes in Computer Science,
Springer-Verlag, July 1996.

**
Nikolaj Bjørner, Anca Browne, Eddie Chang, Michael Colón,
Arjun Kapur, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe
Computer Science Department, Stanford University
Stanford, CA 94305
**

The Stanford Temporal Prover, STEP, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems. STEP uses verification rules, verification diagrams, automatically generated invariants, model checking, and a collection of decision procedures to verify finite- and infinite-state systems.

System Description
The Stanford Temporal Prover, STEP, supports the computer-aided
formal verification of reactive, real-time (and, in particular, concurrent)
systems based on temporal specifications.
Reactive systems maintain an ongoing interaction with their environment;
their specifications
are typically expressed as constraints on their
behavior over time.
STEP is not restricted to finite-state systems, but combines
algorithmic and deductive methods to allow the verification of a broad
class of systems, including parameterized (*N*-component) circuit
designs, parameterized (*N*-process) programs, and programs with
infinite data domains.

The deductive methods of STEP verify
temporal properties of systems by means of verification
rules and verification diagrams. *Verification rules* are used to
reduce temporal properties of systems
to first-order verification conditions [8].
*Verification diagrams* [7, 3]
provide a visual language for guiding, organizing, and displaying
proofs. Verification diagrams allow the user to construct proofs
hierarchically, starting from a high-level, intuitive proof sketch
and proceeding incrementally, as necessary, through layers of greater detail.

Deductive verification almost always relies on finding, for a given
program and specification,
suitably strong auxiliary invariants and intermediate assertions.
STEP implements a variety of techniques for automatic
*invariant generation*. These methods include *local*, *linear* and *polyhedral*
invariant generation,
which perform an approximate, abstract propagation through the system
[2].
Verification conditions can then be established using the
automatically generated auxiliary invariants as background properties.

STEP also provides an integrated suite of simplification and decision procedures for automatically checking the validity of a large class of first-order and temporal formulas. This degree of automated deduction is intended to efficiently handle most verification conditions that arise in deductive verification. An interactive Gentzen-style theorem prover and a resolution-based prover are available to establish the verification conditions that are not proved automatically.

Verification diagrams are also being generalized from [7] to handle arbitrary temporal properties [3] and work is under progress to extend the techniques to modular verification and apply diagram transformations to automate generation of verification diagrams.

**Figure 1:** An overview of the STEP system

**System Structure:**
Fig. 1 presents an overview of STEP.
Dotted lines indicate work in progress.
The basic inputs are a reactive system
(which can be a hardware or software description),
expressed as a transition system,
and a system property to be proved, represented by a temporal logic formula. Verification can be performed
by the model checker or by deductive means.
User guidance can be provided as intermediate assertions or verification diagrams.
In either case, the system is responsible for generating and proving all of the
required verification conditions.
An interactive Gentzen-style theorem prover
and a resolution-based prover are
available to establish the verification conditions that are not proved automatically.
Tactics are available to automate parts of the high-level proof
search by encoding long or repetitive sequences of proof commands.
For a more extensive description of
STEP and examples of verified programs, see [1, 6].

**Interacting with STEP:**
STEP has three main interface components: the
*Top-level Prover*, from which verification sessions are
managed and verification rules are invoked;
the *Interactive Prover*, used to prove the validity of first-order and
temporal-logic formulas that are not proved automatically;
and the *Verification Diagram Editor*, for the creation
of Verification Diagrams.
Fig. 2 shows these three interfaces, with
a version of the Bakery algorithm loaded, together with a tree representing the ongoing proof process.

**Figure 2:** Overview of STEP's interfaces

**Real-time systems:**
STEP was recently extended to support the verification of safety
properties of real-time systems, based on the computational model
of *clocked transition systems* [9].
Systems described by
timed transition systems or
timed automata can be readily translated into this formalism.
The specification language of linear-time temporal logic was
extended, in turn, with real-valued clocks measuring progress of time.

**Applications:**
STEP has been used to analyze a diverse number of systems, including:
an infinite-state demarcation protocol used in
distributed databases, a pipelined four-stage multiplication
circuit, Ricart and Agrawala's mutual exclusion protocol,
several (*N*-component) ring arbiters,
Szymanski's *N*-process mutual-exclusion algorithm, and
an industrial split-transaction bus protocol to coordinate
access for six processors. Real-time systems
analyzed include Fisher's mutual-exclusion protocol and a
(parameterized) railroad gate controller [5].

Simpler examples suited for first-time exposure to
STEP's methodologies include Peterson's, Dekker's, Dijkstra's and
Lamport's (Bakery) algorithms for mutual exclusion, an *N*-process
parking algorithm, a fault tolerant mutual exclusion algorithm,
solutions to the *N*-process dining philosopher's
problem, and Milner's *N*-process scheduler.

STEP is being extended to support
*deductive model checking* as described in
[10], as well as
modular verification diagrams [4].

Educational Version An educational version of the system, which accompanies the textbook [8], is available. The distribution includes a comprehensive user manual [1] and a tutorial, as well as 40 example programs and their specifications, from the textbook, ready to be loaded. For many programs, ready-to-load verification diagrams are included as well.

STEP is implemented in Standard ML of New Jersey, using CML and eXene for its X-windows user interface. An educational version of the system is currently available accompanied by a user's manual providing documentation and a tutorial. For information on obtaining the system, send e-mail to step-request@cs.stanford.edu.

Sat Jun 14 00:06:49 PDT 1997