Project Title: Logical Support for High-Assurance Software Evolution
Organization: Kansas State University
AO Number: E367
Contract Number: CCR-9633388
Start Date: 01 SEPT 1996
End Date: 31 AUG 1998

Principal Investigator

Name:

David     Schmidt
Address: Computing and Information Sciences Department
  234 Nichols Hall, Kansas State University
City,  State   Zip: Manhattan,   KS     66506
Phone: 785-532-6350
Fax: 785-532-7353
Email: schmidt@cis.ksu.edu
Level Of Participation - Billed: 100%
Level Of Participation - Unbilled: %
 

Name:

Matthew     Dwyer
Address: Computing and Information Sciences Department
  234 Nichols Hall, Kansas State University
City,  State   Zip: Manhattan,   KS     66506
Phone: 785-532-6350
Fax: 785-532-7353
Email: dwyer@cis.ksu.edu
Level Of Participation - Billed: 100%
Level Of Participation - Unbilled: %
 

Name:

Allen     Stoughton
Address: Computing and Information Sciences Department
  234 Nichols Hall, Kansas State University
City,  State   Zip: Manhattan,   KS     66506
Phone: 785-532-6350
Fax: 785-532-7353
Email: allen@cis.ksu.edu
Level Of Participation - Billed: 100%
Level Of Participation - Unbilled: 0%
 

Financial POC

Name:

Shannon     Fisher
Address: KSU
  10 Anderson Hall
City,  State   Zip: Manhattan,   KS     66506
Phone: 785-532-6207
Fax: 785-532-5577
Email: fisher@ksu.edu
 
Project URL: http://www.cis.ksu.edu/~schmidt/projects/NSF-CCR-9633388.html
Objective:

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;

Approach: 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.

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.

Recent Accomplishments:

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.

Current Plan:

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.

Technology Transition:

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

Comments / Questions / Anything else you need: This project is funded jointly by NSF (62.2%) and EDCS (37.8%). The above listings of the PIs' Levels of Participation should be stated more precisely as 100% Billed in summer months, 10% Unbilled in Academic Year, which is the norm for NSF-funded projects.