High-Assurance Software Evolution: 1996 Report

AO number: E367


Methodologies and tools will be implemented to help automate consistency checking of module linkages. Data-flow algorithms will be synthesized to analyze individual modules for consistency with respect to local specifications, and a linking manager tool will be used to check for consistency between module specifications. The end result is a combination of automated and user-directed tools to ensure consistency of module linkages thoughout the evolution of complex systems.


Analysis of individual modules in a system will be undertaken by a partial-evaluation-driven abstract-interpretation algorithm. The use of partial evaluation to handle unresolved external module references is novel and crucial to performing a terminating analysis that yields nontrivial local flow information. The use of abstract interpretation to generate the flow analysis guarantees correctness of the information calculated. The result of the analysis is a ``template'' of external flow requirements, formatted to allow further processing at module linkage time.

Consistency checking of the templates generated from analysis of the independent modules will be handled by a linking and configuration manager. The manager will be a combination of automated data-flow analysis techniques and user-interactive type-theory-based realizability tools. The configuration manager will check linkage templates and synthesize common additional code that may be needed to construct valid linkages. It is essential for application to large-scale, evolving systems that link updating must be a local process, so that small changes to the overall system do not incur large penalties. Recent experience with building efficient, usable logic tools will be applied to satisfying these requirements.

Recent 1996 accomplishments

New Start

1997 Plan

Technology transition

New Start


The project is funded jointly by the National Science Foundation and DARPA under the Evolutionary Design of Complex Software initiative.


Prepared by David Schmidt (schmidt@cis.ksu.edu), 01 August 1996