High-Assurance Software Evolution

Logical Support for High-Assurance Software Evolution
01 September 1996 through 31 August 1998
Grant Number:
Matthew Dwyer, Brian Howard, David A. Schmidt, Allen Stoughton
Kansas State University
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 will be myriad opportunities for invalidation of prior assumptions used in code development.

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

1996 Project Summary
1997 Project Summary
1998 Project Summary

Related Links

Prepared by David Schmidt (schmidt@cis.ksu.edu), 16 July 1998