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.