NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Explaining Synthesized SoftwareMotivated by NASA's need for high-assurance software, NASA Ames' Amphion project has developed a generic program generation system based on deductive synthesis. Amphion has a number of advantages, such as the ability to develop a new synthesis system simply by writing a declarative domain theory. However, as a practical matter, the validation of the domain theory for such a system is problematic because the link between generated programs and the domain theory is complex. As a result, when generated programs do not behave as expected, it is difficult to isolate the cause, whether it be an incorrect problem specification or an error in the domain theory. This paper describes a tool we are developing that provides formal traceability between specifications and generated code for deductive synthesis systems. It is based on extensive instrumentation of the refutation-based theorem prover used to synthesize programs. It takes augmented proof structures and abstracts them to provide explanations of the relation between a specification, a domain theory, and synthesized code. In generating these explanations, the tool exploits the structure of Amphion domain theories, so the end user is not confronted with the intricacies of raw proof traces. This tool is crucial for the validation of domain theories as well as being important in everyday use of the code synthesis system. It plays an important role in validation because when generated programs exhibit incorrect behavior, it provides the links that can be traced to identify errors in specifications or domain theory. It plays an important role in the everyday use of the synthesis system by explaining to users what parts of a specification or of the domain theory contribute to what pieces of a generated program. Comments are inserted into the synthesized code that document these explanations.
Document ID
20020061318
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
VanBaalen, Jeffrey
(NASA Ames Research Center Moffett Field, CA United States)
Robinson, Peter
(RECOM Technologies, Inc. Moffett Field, CA United States)
Lowry, Michael
(NASA Ames Research Center Moffett Field, CA United States)
Pressburger, Thomas
(RECOM Technologies, Inc. Moffett Field, CA United States)
Lau, Sonie
Date Acquired
August 20, 2013
Publication Date
January 1, 1998
Subject Category
Computer Programming And Software
Funding Number(s)
CONTRACT_GRANT: NAS2-14217
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Available Downloads

There are no available downloads for this record.
No Preview Available