SHF: Small: Pushing the Frontier of Linear-Time Model-Checking Technology

SHF：小型：推动线性时间模型检查技术的前沿

• 批准号: 1319459
• 负责人: Moshe Vardi
• 金额: $ 30.46万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319459&HistoricalAwards=false
• 关键词: SHF; Small; Pushing; Frontier; Linear

Model checking is a technique for verifying the correctness of computer systems. Different implementations are in wide industrial usage today. There are still, however, many large gaps in our understanding of the algorithmic issues involved in model checking, and the technology is still greatly challenged by industrial designs. For example, in hardware-design verification, it is rarely possible to apply existing tools to complete units with clear functionality. This project is pushing the frontier of this technology with the goal of scaling its applicability to functional system units by developing novel scalable algorithms for model checking. The result will be increased reliability of computer systems. This project will explore the mathematical approach to design verification that uses automata theory as a unifying paradigm for design specification and verification. 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 questions about automata, yielding clean and asymptotically optimal algorithms. While the fundamental theory is well understood, there are still many challenging gaps and improved algorithms can enhance the scalability of this approach significantly. This project investigates ways of improving automata-theoretic algorithms so they are more suitable for model checking at scale.

模型检查是一种用于验证计算机系统正确性的技术。如今，不同的实施方式正在广泛使用。但是，在我们对模型检查中涉及的算法问题的理解中，仍然存在许多巨大差距，而且该技术仍然受到工业设计的挑战。例如，在硬件设计验证中，很少能将现有工具应用于具有清晰功能的单元。该项目正在推动该技术的前沿，以通过开发新颖的可扩展算法进行模型检查来扩展其对功能系统单元的适用性。结果将是提高计算机系统的可靠性。该项目将探索使用自动机理论作为设计规范和验证的统一范式的数学设计验证方法。自动理论方法将有关系统推理的逻辑和组合方面分开。自动机的规范的翻译可以处理逻辑，并将所有组合困难转移到有关自动机的问题上，从而产生清洁和渐近的最佳算法。尽管人们对基本理论的理解有充分的理解，但仍然存在许多具有挑战性的差距，改善的算法可以显着增强该方法的可扩展性。该项目研究了改进自动机理论算法的方法，因此它们更适合于模型进行大规模检查。