Model Checking of Software Systems

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

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. ***