Model Checking of Software Systems

软件系统在规模和复杂性上都在不断增长。我们对这类系统的依赖也在增加，这使得它们遵守设计者预期的属性变得至关重要。因为这些属性是全局的，所以它们的考虑不能留给模块的实现；相反，它们必须在早期通过设计来确保。因此，实现关键属性依赖于能够分析设计，以便可以在不花费实现成本的情况下探索设计选择的后果，并且可以在修复它们的成本仍然相对较低的情况下捕获潜在的灾难性缺陷。基于正式技术而不是非正式技术的分析方法容易受到机械推理的影响。形式化方法在硬件验证中产生了巨大的影响--主要是由于模型检查的成功--并正在被业界采用。另一方面，在软件开发中，形式化方法还没有产生同样的影响。这在很大程度上是因为几乎没有可用的工具支持。几乎任何软件规范的分析似乎都需要定理证明。对于大多数软件开发来说，定理证明是不可行的，因为它需要高技能的证明专家，而且不能完全自动化。如果没有自动分析，形式化规范对实践者来说就不那么有吸引力了。这个项目有两个方面。首先，研究了模型检测技术在软件中的应用。这既包括识别大型系统的适当抽象表示，以及它们应该遵守的属性，也包括发明新的抽象技术以将这些表示与软件设计联系起来。本研究中追求的抽象技术以三种方式产生：(1)来自要检查的属性的形式(例如，合并状态以保留通用量化的属性)；(2)来自应用领域(例如，不区分分布式系统中的故障种类)；以及(3)来自应用本身(例如，在高速缓存协议的评估中抽象高速缓存线中保存的数据)。其次，新的检查技术正在为模型检查目前不能很好地服务的规范而开发。软件设计通常涉及对隐式定义的复杂数据结构的操作。在这种情况下，没有明显的模型需要检查；相反，有必要从规范生成模型，并确定它们是否满足预期的属性。该项目正在开发一种语言NP，它大致是Z规范语言的子集，以及一个检查器Nickick，它既可以模拟隐式指定的操作的执行，又可以通过生成关系公式的模型来检查操作的归纳属性。在强调有望得到更广泛应用的原则的同时，该项目还受到现实案例研究的推动：铁路交换、电话功能和安全协议。***

Software systems keep growing in size and complexity. Our reliance on such systems is likewise increasing, making it critical that they obey the properties their designers intended. Because these properties are global, their consideration cannot be left to the implementation of modules; rather, they must be ensured by design early on. Achieving critical properties thus depends on being able to analyze designs, so that the consequences of design choices can be explored without the cost of implementation, and potentially disastrous flaws can be caught while their repair is still relatively cheap. Analysis methods based on formal, rather than informal, techniques are amenable to mechanical reasoning. Formal methods have had a dramatic impact in hardware verification -- principally due to the success of model checking -- and are being adopted by industry. In software development, on the other hand, formal methods have not yet had the same impact. This is largely because little tool support has been available. Almost any analysis of a software specification seems to require theorem proving. Theorem proving is not feasible for most software developments, since it requires highly skilled proof experts, and cannot be automated fully. Without automatic analysis, formal specification is much less attractive to practitioners. This project has two aspects. First, it investigates the application of model checking techniques to software. This involves both the identification of appropriate abstract representations of large systems, along with the properties they should obey, and the invention of new abstraction techniques to relate such representations to software designs. The abstraction techniques pursued in this research arise in three ways: (1) from the form of the property to be checked (for example, merging states to preserve a universally quantified property); (2) from the application area (for example, not distinguishing the varieties of failure in a distribu ted system); and (3) from the application itself (for example, abstracting the data held in cache lines in the evaluation of a cache protocol). Second, new checking techniques are being developed for specifications that are not currently well served by model checking. Software designs often involve operations on complex data structures that are defined implicitly. In this case, there is no apparent model to be checked; rather, it is necessary to generate models from the specification and determine whether they satisfy intended properties. The project is developing a language, NP, that is roughly a subset of the Z specification language, and a checker, Nitpick, that can both simulate the execution of operations specified implicitly and check inductive properties of operations, by generating models of a relational formula. While emphasizing principles that are expected to find broader application, the project is driven by realistic case studies: railway switching, telephone features, and security protocols. ***