1997 Project Summary
High-Assurance Software Evolution
Kansas State University
ARPA Order No. E367

Research Data
Related Information /
Project URL:
http://www.cis.ksu.edu/~schmidt/projects/NSF-CCR-9633388.html -- Additional project information provided by the performing organization
Objective: Consistency checking of interfaces in evolving modular systems is addressed: The goal is to provide a combination of manual and automated techniques to maintain a system as its components evolve. Foundational and experimental techniques from the area of meta-programming are employed to develop tools that (i) statically analyze components and synthesize interface information; (ii) link components and create linkage code (``smart glue'') to reconcile mismatches; (iii) tightly bind components at their interface points to reduce run-time overhead.
Approach: Meta-programming is the study of ``programming on programs''; it encompasses static analysis, program transformation, and program synthesis. The key components of meta-programming used in this project are abstract interpretation and partial evaluation, but related techniques such as model checking and proof search are also employed.

First, static analysis of individual components is performed by a partial-evaluation-driven abstract interpreter, which generates a finite-state abstraction of a component that can be model checked for validity or data-flow analyzed to synthesize an interface. The combination of partial evaluation with abstract interpretation lets individual components be analyzed with a precision that is similar to that of an analysis of an entire system. Next, techniques from proof search and realizability theory are used to check compatibility of components' interfaces and automatically generate module linkage code when the interfaces do not match precisely. Finally, interface points and their linkage code are tightly bound by a partial evaluator customized for modular, distributed systems. This makes practical the use of large numbers of components in a complex system.

Recent FY-97 Accomplishments:

Developed a theoretical basis (filter-based abstract interpretation) that underlies a class of abstraction-based static program analyses, including FLAVERS.

Developed an approach to model checking and flow analysis of incomplete software systems using partial specification of missing components.

Implemented a partial evaluator for state analysis of program components.

Formulated a theory of trace-based abstract interpretation for justifying static analyses.

FY-98 Plans:

Apply the abstract interpreter for system components to nontrivial test cases, developing further domain-specific abstractions and providing support for automating analysis based on those abstractions.

Adapt model checking and abstract interpretation technology to FLAVERS/Ada, a data-flow analysis tool for analyzing modules in isolation and in linkage with subsystems. Enable static analysis of programs with dynamic control and data components.

Develop a prototype implementation of a system for automatically synthesizing module linkage code in limited cases.

Prototype a partial evaluator for tightening linkage bindings in modular and distributed systems.

Technology Transition:
Principal Investigator: David Schmidt
Computing and Information Sciences Department
234 Nichols Hall, Kansas State University
Manhattan, Kansas 66506
(913)532-7353 fax
Co-Principal Investigator: Matthew Dwyer
Computing and Information Sciences Department
234 Nichols Hall, Kansas State University
Manhattan, Kansas 66506
(913)532-7353 fax
Co-Principal Investigator: Brian Howard
Department of Mathematics and Computer Science
Box 81, Bridgewater College
Bridgewater, Virginia 22812
(540)828-5479 fax
Co-Principal Investigator: Allen Stoughton
Computing and Information Sciences Department
234 Nichols Hall, Kansas State University
Manhattan, Kansas 66506
(913)532-7353 fax

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

Quad Chart