Automata-Theoretic Approach to Design Verification

William Marsh Rice University, Houston TX

Investigators

Abstract

The objective of the proposed research is the development of algorithmic methods for design verification. Today's rapid development of complex and safety-critical systems requires reliable verification methods. Formal verification is the study of algorithms and structures applicable to the verification of hardware and software designs. It combines theoretical and experimental aspects. In the last few years, this area has seen a dramatic expansion of activities. Verification tools are incorporated into industrial development of new designs, forming an active and exciting area of research where theory and practice stimulate each other. The intellectual merit of this poject is the application of the automata-theoretic approach to design verification, which uses the theory of automata as a unifying paradigm for design specification, verification, and synthesis. The automata-theoretic perspective considers the relationships between designs and their specifications as relationships between languages. By translating design and logical specifications to automata, questions about programs and their specifications can be reduced to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of designs with respect to their specifications can be reduced to questions such as non-emptiness and containment of automata. The automata-theoretic approach separates the logical and the combinatorial aspects of reasoning about systems. The translation of specifications to automata handles the logic and shifts all the combinatorial difficulties to automata-theoretic problems, yielding clean and asymptotically optimal algorithms. Furthermore, automata are very helpful for implementing temporal-logic based verification methods, and are the key to techniques such as on-the-fly verification that help coping with the ``state-explosion'' problem. Automata-theoretic methods have been implemented in both academic and industrial automated-verification tools. Many questions in the theory of automata on infinite objects are still open, and more fruitful applications of automata theory in design verification are possible. This projects aims at solving several automata-theoretic problems with clear application to design verification, and at develoing automata-based verification methodologies. The broad impact of this project is the contribution to the efforts of developing and improving formal verification methods, constituting an additional step toward formal verification of industrial real-life designs.