REACT group 1996 DARPA/ITO Research Project Summary
Software Development Technologies For Reactive, Real-Time, 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 high-assurance systems, especially reactive (concurrent, real-time,
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, real-time, 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 first-order logic,
allowing the verification and development of a broad class of systems,
including parameterized (N-component) circuit designs, parameterized
(N-process) programs, and infinite-state systems
(e.g., programs with infinite data domains).
A complementary approach to deductive verification is algorithmic
verification (model checking), where graph-search techniques and
specialized data structures are used to explore the state-space of
the system being verified.
Unlike deductive methods, which are interactive in general, model checking
is automatic; however, it is usually restricted to finite-state systems
and suffers from the state-explosion 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 infinite-state
reactive systems. Local transformations are applied to an abstraction
of the product graph, in search for a counter-example computation.
This approach combines advantages of deductive and algorithmic verification:
like model checking, the process is goal-directed and incremental,
and can produce a counter-example
when the property does not hold; like deductive verification, it can handle
infinite-state systems, and produces a proof object if the property holds.
User input can direct the search for a
counter-example and help rule out large portions of the search
space before they are expanded to the state level, combating the
state-space explosion problem common in model checking.
This procedure has been implemented in conjunction with
the STeP verification system (below).
Diagram-based Verification:
Verification Diagrams provide a visual language
for guiding, organizing, and displaying verification proofs.
They allow constructing proofs hierarchically, starting from a
high-level 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 linear-time 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 omega-automata,
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 real-time systems; improved interfaces
for the non-clausal resolution-based 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 e-mail to step-request@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 user-guidance) verification diagrams
for the verification of infinite-state systems or abstractions of large
finite-state 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 counter-example
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 automata-theoretic (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 e-mail to step-request@CS.Stanford.EDU.
(See also
http://www-step.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 infinite-state demarcation protocol used in distributed data bases,
a pipelined four-stage multiplication circuit suggested as a challenge by INTEL,
Ricart and Agrawalla'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 of six processors provided by SUN Microsystems.
Real-time systems analyzed include Fisher's mutual-exclusion protocol
and a (parameterized) railroad gate controller.
Analysis of Szymanski's algorithm uncovered a flaw in the
pre-published version of the paper. This bug was corrected
following our suggestions in the final published version.
Back to the REACT research group page.