REACT group 1996 DARPA/ITO Research Project Summary
Software Development Technologies For Reactive, RealTime, and Hybrid Systems
DARPA/ITO 1996 Research Project Summary
Objective:
The research is directed towards the design and implementation
of a comprehensive deductive environment for the development
of highassurance systems, especially reactive (concurrent, realtime,
and hybrid) systems. Reactive systems maintain an ongoing interaction
with their environment, and are among the most difficult to design
and verify. The project aims to provide engineers with a wide variety
of tools within a single, general, formal framework in which the
tools will be most effective.
The entire development process is considered, including the construction,
transformation, validation, verification, debugging, and maintenance
of computer systems. The goal is to automate the process as much as
possible and reduce the errors that pervade hardware and software development.
Approach:
The formal framework is based on the generic computational model
of Transition Systems, specialized to Fair Transition Systems, Timed
Transition Systems, and Phase Transition Systems for the classes of
concurrent, realtime, and hybrid systems, respectively. These models
cover both hardware and software systems, and underlie all the
proposed languages and methods. The most complex of these models,
phase transition systems, combines discrete transition systems with
continuous processes whose parameters are controlled by differential equations.
Deductive verification uses the expressive power of firstorder logic,
allowing the verification and development of a broad class of systems,
including parameterized (Ncomponent) circuit designs, parameterized
(Nprocess) programs, and infinitestate systems
(e.g., programs with infinite data domains).
A complementary approach to deductive verification is algorithmic
verification (model checking), where graphsearch techniques and
specialized data structures are used to explore the statespace of
the system being verified.
Unlike deductive methods, which are interactive in general, model checking
is automatic; however, it is usually restricted to finitestate systems
and suffers from the stateexplosion problem. We are integrating
model checking and deduction into one framework, thus
combining the expressiveness of deductive methods with the simplicity
of model checking.
Recent 96 Accomplishments:
Combining Deductive and Algorithmic Methods:
We have developed deductive model checking, a variant of classical model
checking that allows the verification of general infinitestate
reactive systems. Local transformations are applied to an abstraction
of the product graph, in search for a counterexample computation.
This approach combines advantages of deductive and algorithmic verification:
like model checking, the process is goaldirected and incremental,
and can produce a counterexample
when the property does not hold; like deductive verification, it can handle
infinitestate systems, and produces a proof object if the property holds.
User input can direct the search for a
counterexample and help rule out large portions of the search
space before they are expanded to the state level, combating the
statespace explosion problem common in model checking.
This procedure has been implemented in conjunction with
the STeP verification system (below).
Diagrambased Verification:
Verification Diagrams provide a visual language
for guiding, organizing, and displaying verification proofs.
They allow constructing proofs hierarchically, starting from a
highlevel intuitive sketch and proceeding incrementally, as necessary,
through layers of greater detail. We have developed Generalized
Verification Diagrams, which give a sound and complete method for
proving general lineartime temporal properties of systems.
Generalized Verification Diagrams have been further extended to support
modularity, facilitating the verification of large and complex systems,
and allowing the verification of properties expressable by omegaautomata,
a strictly larger class than those verifiable by usual verification diagrams.
We have also developed Fairness Diagrams, an extended graphical
representation used to incrementally abstract and refine systems
until they are amenable to automatic verification.
The STeP System:
Continued developing and improving the
STeP verification system.
Among these improvements are: stronger decision procedures;
rules for modular verification; visual representation of proof searches;
support for the verification of realtime systems; improved interfaces
for the nonclausal resolutionbased theorem proving component.
We have applied STeP to verification problems of interest to companies
such as INTEL and SUN.
An educational version of STeP has been released, and is being used
by a number of groups around the world.
(To obtain STeP, send email to steprequest@cs.stanford.edu.)
A new release of STeP is scheduled for November, 1996.
FY1997 Plan:

Continue to develop visual formalisms for verification. This includes:
(1) using our deductive model checking techniques to construct
(automatically or with minimal userguidance) verification diagrams
for the verification of infinitestate systems or abstractions of large
finitestate systems; and (2) combining the complementary proof
methodologies of deductive model checking and fairness diagrams.
While the first method proves a property by searching for a counterexample
computation, the second can be used to transform and abstract a
system directly, independently of any property to be proved.
We expect that combining the two approaches in a single framework will
enable modular and incremental analysis of large systems.

Extend the STeP system to handle hybrid systems. This includes identifying the
most suitable formalisms for encoding hybrid systems and their properties,
and generating the corresponding verification conditions in an
extended language. This language will be able to express the
differential equations, limits and derivatives, that arise from the
verification of hybrid systems. We will investigate the applicability of
different symbolic computation procedures in the analysis of such
formulas, as well as the use of numerical solutions and approximations.

Continue to investigate reactive synthesis.
A challenging alternative to verification is the direct
synthesis of programs and systems based on their specifications.
We are exploring automatatheoretic (algorithmic) synthesis of reactive
systems, including methodologies that will make such algorithms usable
in practical examples.
We are collaborating with industrial partners interested in applying
synthesis technology to the development of control programs.
We are also continuing research in deductive synthesis of functional
programs and its relationship to verification,
building on the deductive mechanisms available in the STeP system.
Technology Transition:
The STeP system is being used for educational and research purposes
in over 30 sites around the world. At Stanford, STeP and its
deductive components are being used in courses on formal verification
and introductory logic. Information on obtaining the system
is available by sending email to steprequest@CS.Stanford.EDU.
(See also
http://wwwstep.stanford.edu/.)
STeP has been used to verify circuits proposed by Intel and SUN.
We have initiated further industrial collaborations that will explore
how our deductive technology can be applied to complex hardware designs,
which will drive new research and development.
Systems verified successfully with STeP include:
an infinitestate demarcation protocol used in distributed data bases,
a pipelined fourstage multiplication circuit suggested as a challenge by INTEL,
Ricart and Agrawalla's mutual exclusion protocol,
several (Ncomponent) ring arbiters,
Szymanski's Nprocess mutualexclusion algorithm,
and an industrial splittransactionbus protocol to coordinate
access of six processors provided by SUN Microsystems.
Realtime systems analyzed include Fisher's mutualexclusion protocol
and a (parameterized) railroad gate controller.
Analysis of Szymanski's algorithm uncovered a flaw in the
prepublished version of the paper. This bug was corrected
following our suggestions in the final published version.
Back to the REACT research group page.