Model Checking and Beyond

长期以来，人们需要更有效的方法来设计正确和健壮的计算机软件和硬件。发展了一种称为“模型检查”的方法，为确定名义上有限状态程序的正确性提供了一种算法手段。IBM、英特尔和摩托罗拉等计算机制造商发现，模型检查对于验证中等大小的计算机硬件电路很有用。然而，在模型检测能够成功地应用于大型硬件设计和软件之前，还需要进一步的研究。由于软件组织不统一，规模庞大，比硬件更难构造和验证。研究的其他中心课题包括：新的和改进的基本技术，包括抽象、算法和数据结构，以实现更有效的模型检测；模型检测与其他程序设计方法的集成；通过模型检测实现程序自动综合；以及使用更丰富的程序健壮性概念扩展传统模型检测的二分(正确/错误)框架的可行性。

There is a chronic need for more effective methods of designing correct and robust computer software as well as hardware. A method called "Model Checking" has been developed, providing an algorithmic means for establishing correctness of nominally finite state programs. Computer manufacturerssuch as IBM, Intel, and Motorola are finding model checking useful for verifying computer hardware circuits of moderate size. However, further research is required before model checking can be applied successfully to large hardware designs and to software. Software is more difficult to construct and verify than hardware due to its less uniform organization and sheer scale. Techniques to cope with irregular organization based on partial order and asymmetry reduction facilitating application of model checking to large software systems will be investigated.Other central topics of investigation include: new and improved basic techniques, including abstractions, algorithms, and data structures, for more efficient model checking; integration of model checking with other program design methods; automatic program synthesis via model checking; and the feasibility of extending the dichotomous (correct/incorrect) framework of conventional model checking using richer program robustness notions.