Logical Support for High-Assurance Software Evolution

大型软件项目的管理和可重用软件库的维护中的一个中心问题是在面对持续的系统演变时确保模块间连接的一致性。由于错误被隔离和修复，功能被添加或增强以响应用户需求的变化，支持软件和硬件被升级或替换，因此有无数的机会使代码开发中使用的先前假设失效。在这个项目中，来自逻辑、类型理论和抽象解释的技术被用于工具的设计和实现，以帮助自动化确保一致性的过程。使用部分求值驱动的抽象解释算法来分析各个模块与本地规范的一致性，使用链接和配置管理器来检查模块规范之间的对应关系。使用抽象解释、证明生成和可实现技术，管理者综合了可能需要提供可信链接的公共附加代码。这种方法的两个方面对于应用于大规模的、不断发展的系统是必不可少的：(i)链接更新必须是一个局部过程，这样小的变化就不会引起大的损失，（ii）链接信息必须以用户可读的格式提供给程序员。最近在构建高效、可用的逻辑工具方面的经验被应用到项目中，以满足这些需求。* * *

A central problem in the management of large software projects and the maintenance of libraries of reusable software is ensuring the consistency of inter-module connections in the face of continuing system evolution. As bugs are isolated and fixed, capabilities are added or enhanced in response to changes in the user requirements, and support software and hardware is upgraded or replaced, there are myriad opportunities for invalidation of prior assumptions used in code development. In this project, techniques from logic, type theory, and abstract interpretation are employed in the design and implementation of tools to help automate the process of ensuring consistency. A partial-evaluation-driven abstract-interpretation algorithm is used to analyze individual modules for consistency with respect to local specifications, and a linking and configuration manager will be used to check for correspondence between module specifications. Using abstract interpretation, proof generation, and realizability techniques, the manager synthesizes common additional code that may be needed to provide trustworthy linkages. Two aspects of this approach are essential for application to large-scale, evolving systems: (i)link updating must be a local process, so that small changes do not incur large penalties, and (ii)linkage information must be available to the programmer in a user-readable format. Recent experience with building efficient, usable logic tools is applied in the project towards satisfying these requirements. ***