next up previous
Next: References

Computer Science Department, Stanford University Stanford, CA 94305

STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems

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

Abstract:

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.




next up previous
Next: References

step-comments@CS.Stanford.EDU
Sat Jun 14 00:06:49 PDT 1997