Explaining Synthesized Software

Motivated 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 ructures and abstracts them to provide expla...

• Type: Conference
• Year: 1998
• Where: KBSE
• Authors: Jeffrey Van Baalen, Peter Robinson, Michael R. Lowry, Thomas Pressburger
• Keywords: Deductive Synthesis, Domain Theory, Generated Program, KBSE 1998, Software Engineering