High-Assurance Software Evolution High-Assurance Software EvolutionTechniques from logic, type theory, and abstract interpretation will be employed in the design and implementation of tools to help automate the process of ensuring consistency. A partial-evaluation-driven abstract-interpretation algorithm will be 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 will synthesize 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 will be applied to satisfying these requirements.