Model Checking of Software Systems

软件系统的模型检验

• 批准号: 9523972
• 负责人: Jeannette Wing
• 金额: $ 31.7万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-09-01 至 1999-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9523972&HistoricalAwards=false
• 关键词: Model; Checking; Software; Systems

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

软件系统的规模和复杂性不断增长。我们对此类系统的依赖同样也在增加，因此至关重要的是，他们遵守设计师预期的财产。由于这些属性是全球的，因此它们的考虑不能留给模块的实现。相反，必须尽早通过设计来确保它们。 因此，实现关键属性取决于能够分析设计，因此可以在没有实施成本的情况下探索设计选择的后果，并且在维修仍然相对便宜的同时，可以捕获潜在的灾难性缺陷。 基于形式而不是非正式技术的分析方法与机械推理有关。正式方法对硬件验证产生了巨大的影响 - 主要是由于模型检查的成功 - 并被行业采用。另一方面，在软件开发中，正式方法尚未产生相同的影响。这主要是因为几乎没有工具支持。几乎所有对软件规范的分析似乎都需要定理证明。对于大多数软件开发而言，定理证明这是不可行的，因为它需要高技能的证明专家，并且不能完全自动化。 没有自动分析，正式规范对从业者的吸引力要少得多。 该项目有两个方面。 首先，它研究了模型检查技术在软件中的应用。这既涉及识别大型系统的适当抽象表示形式，以及他们应该遵守的属性，以及发明新的抽象技术以将这些表示形式与软件设计联系起来。 在这项研究中采用的抽象技术以三种方式出现：（1）从要检查的财产形式（例如，合并国家以保留普遍量化的财产）； （2）从应用区域（例如，不区分分布系统中的失败品种）； （3）从应用程序本身中（例如，在评估缓存协议中的高速缓存线中固定的数据）。 其次，正在开发针对当前模型检查目前尚未很好地服务的规格开发新的检查技术。软件设计通常涉及对隐式定义的复杂数据结构进行操作。在这种情况下，没有明显的模型可以检查。相反，有必要从规范中生成模型并确定它们是否满足预期的属性。该项目正在开发一种语言NP，该语言大约是Z规范语言的子集，以及Checker nitpick，可以通过生成关系公式的模型来模拟指定的操作的执行和检查操作的归纳属性。 在强调预期会找到更广泛应用的原则的同时，该项目是由现实的案例研究驱动的：铁路切换，电话功能和安全协议。 ***