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