Automata-Theoretic Approach to Design Verification

设计验证的自动机理论方法

• 批准号: 0311326
• 负责人: Moshe Vardi
• 金额: --
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-07-15 至 2007-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0311326&HistoricalAwards=false
• 关键词: Automata; Theoretic; Approach; 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.

提出的研究目标是设计验证的算法方法的发展。当今复杂和安全关键系统的快速发展需要可靠的验证方法。形式验证是对适用于硬件和软件设计验证的算法和结构的研究。它结合了理论和实验两个方面。在过去几年中，这一领域的活动急剧扩大。验证工具被整合到新设计的工业开发中，形成了一个活跃而令人兴奋的研究领域，理论和实践相互促进。这个项目的智力优点是将自动机理论方法应用于设计验证，它使用自动机理论作为设计规范，验证和综合的统一范式。自动机理论认为设计和规范之间的关系就像语言之间的关系一样。通过将设计和逻辑规范转换为自动机，有关程序及其规范的问题可以简化为有关自动机的问题。更具体地说，诸如规范的可满足性和设计的正确性等问题可以简化为诸如非空性和自动机的包含性等问题。自动机理论的方法分离了系统推理的逻辑和组合方面。将规范转换为自动机处理逻辑，并将所有组合困难转移到自动机理论问题，从而产生干净且渐近最优的算法。此外，自动机对于实现基于时间逻辑的验证方法非常有帮助，并且是处理“状态爆炸”问题的实时验证等技术的关键。自动机理论方法已经在学术和工业自动化验证工具中得到了应用。无限大对象自动机理论中的许多问题仍有待解决，自动机理论在设计验证中的更富有成效的应用是可能的。本项目旨在解决几个具有明确应用于设计验证的自动机理论问题，并开发基于自动机的验证方法。这个项目的广泛影响是对开发和改进形式化验证方法的贡献，构成了对工业现实设计的形式化验证的额外步骤。