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
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
Design and implementation of a partial-evaluation-driven abstract
interpreter for analysis of independent modules and generation of
Testing of FLAVERS/Ada, a data-flow analysis
tool for analyzing modules in isolation and in linkage with
Application studies of Porgi, a proof synthesizer for propositional
intuitionistic logic, to consistency checking of linkages
of module specifications
The project is funded jointly by the National Science Foundation and
DARPA under the Evolutionary Design of Complex Software initiative.
David Schmidt (email@example.com), 01 August 1996