Automata-Theoretic Approach to Design Verification

点击翻译按钮获取中文摘要

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 theautomata-theoretic approach to design verification, which uses the theoryof automata as a unifying paradigm for design specification,verification, and synthesis. The automata-theoreticperspective considers the relationships between designs and theirspecifications as relationships between languages. By translatingdesign and logical specifications to automata, questions aboutprograms and their specifications can be reduced to questions aboutautomata. More specifically, questions such as satisfiability ofspecifications and correctness of designs with respect to theirspecifications can be reduced to questions such as non-emptiness andcontainment 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 implementingtemporal-logic based verification methods, and are the key to techniques such as on-the-fly verificationthat 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 stillopen, and more fruitful applications of automata theory in designverification are possible. This projects aims at solving severalautomata-theoretic problems with clear application to designverification, and at develoing automata-based verification methodologies.The broad impact of this project is the contribution to theefforts of developing and improving formal verification methods,constituting an additional step toward formal verification ofindustrial real-life designs.