REACT group 1996 DARPA/ITO Research Project Summary

Software Development Technologies For Reactive, Real-Time, and Hybrid Systems

DARPA/ITO 1996 Research Project Summary

Zohar Manna
Computer Science Department
Stanford University
Stanford, California 94305-9045


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.


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:

FY1997 Plan:

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

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.