Conference turris::languages

379.0. "Knowledge based software process automation at Kestrel" by STAR::PRAETORIUS (I have faith in questioning) Wed Jun 29 1994 01:19

[from http://kestrel.edu/pub/mosaic/research-areas.html ,
 home page is http://kestrel.edu/pub/mosaic/kestrel.html .
 cross posted to Turris::Languages, Ricks::Formal_Verification
 and Cookie::Formal_Methods ]


Kestrel Research Areas



Language Design 

A central issue is the design of very-high-level and wide-spectrum
languages, for specifying both programs and software knowledge in
general. We are investigating iteration constructs, abstract data types,
and concurrency constructs. 

Algorithm Design

A few fundamental algorithm schemes, such as generate-and-test,
branch-and-bound, divide-and-conquer, dynamic programming, and
hill-climbing, explain a great number of known algorithms. We are
codifying these algorithm design schemes so that these kinds of
algorithms can be automatically derived for a given very-high-level
problem specification, when given appropriate domain axioms. 

Transformational Compilation

Our work is concerned with techniques for optimizing algorithms. We
have been investigating performance-estimation-guided data structure
synthesis, finite differencing (a generalization of traditional strength
reduction), loop fusion, iterator inversion, and constraint compilation.
Software Engineering Environments: We are developing a formal
environment model that allows the description of all objects,
operations, and tools involved in software engineering environments.
Based on such a model, we represent environment objects and their
properties in a knowledge base. It will be possible within this
framework to use our program transformation and synthesis
technology to generate procedures to build new versions of a system,
to generate releases, or to perform a maintenance step. Thus, by
representing the life-cycle itself as a formal program, we can
transform the life-cycle to achieve major optimizations. 

Inference

Our algorithm design schemes require various forms of inference, such
as finding necessary or sufficient conditions, simpler equivalents, or
lower bounds. We are continuing to develop a deduction system that
we have built to do this. We are also investigating algorithms for
constraint satisfaction and special purpose reasoning. 

Graphics

Graphical display of data is a large part of software systems and
thus accounts for a significant portion of the cost of developing and
maintaining software. We are working on a theoretical and practical
basis for the generation of software for tabular and graphical
displays. The effort consists of two theories to account for the
generation of possible displays of given data, and the selection of an
appropriate display for the task at hand. 

Requirements

We attempt to apply the results of our research on language design,
time models, and graphics to the specification of functional,
performance, and interface requirements. Together with
domain-specific synthesis (below), emerging tools will considerably
speed up requirements convergence. 

Domain-Specific Synthesis

Here we attempt to codify knowledge that is specific to a particular
application area so that the transformation system can use this
knowledge during the refinement of specifications written in a
domain-specific language. Much like a module encapsulates a
particular data type or algorithm, we introduced the notion of a
knowledge pack that encapsulates generic, reuseable concepts needed
to specify and to solve problems in a particular application domain.