We will describe a mature program synthesis system called Amphion which has been applied to a number of NASA application domains. It enables non-programmer end-users to develop problem specifications graphically, and then generates a program that achieves the specification through a composition of components from a component library. We will focus particularly on Amphion/NAIF, which generates solar system observation opportunity analyzers. For example, suppose a space scientist wants to determine the opportunities for the Cassini spacecraft, while orbiting Saturn, to transmit an unobstructed signal to the Goldstone observatory on earth. Before Amphion/NAIF the scientist was required to write a Fortran program consisting of calls to subroutines in the SPICE library (developed at JPL). Amphion/NAIF provides the space scientist with a high-level graphical editor with which desired observation opportunities can be specified without knowing about the SPICE library. Amphion/NAIF automatically generates required Fortran programs from such specifications. The system also includes an animation component that provides scientifically realistic simulations of generated programs, and a component that explains the synthesized program.
We will then present an overview of Meta-Amphion, a long range research project in the Automated Software Engineering (ASE) group. Meta-Amphion is a system that specializes a deductive synthesis system consisting of a domain theory and a general-purpose theorem prover. The specialization technique takes as input a domain theory and a library of parameterized decision procedures. It identifies instances of the theories of these procedures in the domain theory, interfaces the procedure instances to a refutation-based theorem prover (SNARK from SRI), and often removes the identified axioms from the domain theory. The result is a deductive synthesis system that is specialized to the given domain theory and usually far more efficient than the original system.
We will then describe a case study of verifying components of the Remote Agent, which is an intelligent system developed jointly by Ames and JPL AI researchers to achieve spacecraft autonomy. We were able to identify through model-checking a number of subtle concurrency errors that occurred in the Lisp-based executive portion of the remote agent, which would not have been found in the course of normal testing. Similar errors have previously caused extended loss of spacecraft functions, for example on Mars Pathfinder and the first Brazilian micro-spacecraft. We briefly describe current research to enable this type of formal verification to be used directly by developers.