This NSF/EDCS basic-research project addresses consistency checking of interfaces and static analysis of components of evolving modular systems. The goal is to provide a combination of manual and automated techniques to analyze and maintain a system as its components evolve. Foundational and experimental meta-programming techniques are employed to develop tools that (i) statically analyze components and synthesize interface information and (ii) link components and create linkage code (``smart glue'') to reconcile mismatches;

Abstract interpretation is a semantically safe technique for symbolically executing programs, and partial evaluation is an automated program transformation methodology; the two are combined into a program transformer tool for symbolic execution of incomplete or component-based programs. Importantly, the formal semantics of the ``symbols'' and their ``execution'' are supplied as inputs to the tool, ensuring that the transformation steps taken on an input program are semantically sound. An incremental variant of abstract interpretation, called a filter, lets one tune the symbolic execution to the appropriate precision.

The tool is applied to individual program components. For each component, the tool generates a finite-state abstraction that can be model checked for validity or data-flow analyzed for synthesizing an interface. Here, the novelty is that the finite-state model is an incomplete component, yet it contains useful semantic content.

Say that the issue at hand is validity of the component: the ``gaps'' in the model (that is, the places where missing components should be inserted) are instantiated with semantically sound ``stubs'' so that model-checking tools, such as SPIN and SMV, can be used to check safety conditions.

If the goal is flow analysis of the component, a collecting-semantics tool extracts data-flow information from the model and compresses it into a residual, tabular form. The gaps in the model are encoded as flow functions, which compute on the residual tables at link time.

Program components must be linked, and the interface representations described above---temporal logic formulas and compressed tables---must be linked and computed upon further at link time. Higher-order unification and proof search techniques are used to synthesize linkage code for interfaces.

Developed the theoretical basis, with proved theorems, for the semantic correctness of the approach.

Applied filter-based abstraction interpretation to formulation of models that were model checked with the FLAVERS system and the SPIN model checker. These experiences suggest that filtering is easy for developers to apply, significantly reduces analysis times, and improves the accuracy of analysis results.

Implemented a second experimental prototype that applies abstract interpretation to program components, extracts collecting semantics, and does tabular compression of the collecting semantics.

Designed and partially implemented a system for automatically synthesizing module linkage code for a simple sub-language of Standard ML. A second tool has been prototyped for linkage synthesis of tabular collecting semantics information.

Improve the implementations of finite-state model synthesis tools and linkage tools.

Extend and systematize the library of abstract interpretations for static analyses.

Apply the final toolset to scaled-up applications, including collections of publically available reusable components.

Complete prototype implementation of DOPS, a framework for Deterministic OPerational Semantics, that supports the incremental construction of programs' semantic models.

Provide examples and case studies to NSF Experimental Software Systems Project CCR-9708184 and NASA Project NAG-2-1209 to drive the technology developed in those projects.

Expand interaction with NASA-Ames Automated Software Engineering Group