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