NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

+Intelligent Systems Division

+Robust Software Engineering

+Synthesis Projects & Applications

Amphion: Synthesis of Planetary Software and Animations, and The

Amphion: Synthesis of Planetary Software

Origin of the name "Amphion"

The Greek god Amphion, son of Zeus, charmed the stones lying around Thebes into position to form the city's walls - through the melodious sound of his magic lyre. The Amphion system, developed by the Robust Software Engineering Group at the Computational Sciences division [now named Intelligent Systems Division] of the NASA Ames Research Center, composes software components from libraries into programs that implement users' specifications - through deductive program synthesis by an automated theorem prover.


The goal of the Amphion project is to make Knowledge-Based Software Engineering (KBSE) a reality for NASA. KBSE uses techniques from artificial intelligence and formal methods to raise the level at which users program to the specification level (which describes the problem to be solved) from the code level (which describes how to solve the problem).

The Amphion approach to implementing KBSE for NASA is to automate software reuse. The construction of reuse libraries of software components is the standard software engineering solution for improving software development productivity and quality. By encapsulating usable functionality in software components (e.g. subroutines, object classes), and then reusing those components, software of greater 1functionality can be developed in less time, with some assurance that the overall system is correct because it is built up from trusted components.

However, there are impediments to the reuse of software libraries. Obviously, nonprogrammers cannot use them directly, so some kind of interface must be provided. Even for programmers, there is a barrier in the form of the startup time to learn the library. The library may be inadequately documented, or, on the other hand, may be profusely documented; either is an impediment. All of this is exacerbated because, we claim, conventional high-level languages (e.g. C++) do not provide an interface at a high-enough level. High-level languages, for example, do not allow for the specification of constraints. Components built from such programming languages will necessarily be committed to details below the interest of the end user, e.g. particular data structures, scientific units, mathematical representations. If the language does provide a level above this, efficiency may be lost due to run-time interpretation.

The goals of the Amphion project are to provide a system with the following properties:

  • End-users develop problem specifications via a helpful interface. Specifications, not programs, are maintained.
  • Programs are generated from the specifications by an automatic program synthesis system.
  • The synthesis system is generic, and is targeted to a new domain by the addition of declarative knowledge that component developers, as opposed to KBSE experts, can provide.

To this end, we have created Amphion, which contains a domain-theory driven generic graphical interface and program synthesis system, and Meta-Amphion, which compiles a domain theory into an efficient form. One major application has been an instantiation, called Amphion/NAIF, to particular component libraries critical to NASA's missions in planetary exploration, namely the libraries SPICE, EUCLID/ESCHER, and PERCY, which are Fortran77 libraries created by the NAIF group at JPL. The application domains of these libraries are, respectively, solar system geometry, visualization, and search. The examples below are from this application of Amphion.

Graphical Specifications

Using the Amphion user interface, an end-user can build a graph which represents a high-level specification. Components of the graph for the NAIF domain include planetary, geometric, and kinematic objects, relationships, constraints, and input/output representations. These graphs serve as input to the program synthesis module.

Program Synthesis

The program synthesis module checks some necessary conditions that the high-level specification be solvable, namely, whether it is over- or under-constrained. If it passes these tests, the program synthesis module, using an axiomatization of the subroutine library and the SNARK theorem prover, constructs a concrete program that solves the specification.

Final Programs

The concrete program produced by the theorem prover is then translated into the target language. For the NAIF domain, the target language is Fortran77.


Amphion specifications can also specify a visualization of the appearance of a solar system scene at a particular time. The Amphion-generated program calls rendering subroutines in the Escher and Euclid libraries, which were created by the NASA Jet Propulsion Laboratory NAIF group. Steve Roach adapted the routines to display to an X window, and he built an interface to call the visualization program repeatedly while incrementing time, thus creating a solar system animator.

One visualization we specified was designed to help planetary scientists working on the Cassini mission to Saturn evaluate whether proposed tours could satisfy their observational requirements. The visualization is the view the Cassini spacecraft would have of Saturn and its moon Titan. Below, we present excerpts from the animations.

Amphion's animation capability also helped Dr. Mark Showalter with the creation of the popular Saturn viewer, which was developed for use during the time Saturn's ring plane crossed the Earth. Initial programs were generated from an informational specification (GIF, 28K) for calculating various desired quantities, e.g. the scattering and opening angles, and a visualization specification (GIF, 28K) of the view of Saturn from the Earth.

For this application, Amphion's theory of the NAIF library was inadequate in that it did not deal with stellar aberration, so he modified slightly the Amphion-generated program. We are working to make it easy to extend the domain theory, so that component developers can extend it themselves. Dr. Showalter also extended the Euclid library to draw labels on its graphs and show certain shadows, and, of course, made these programs accessible from the World Wide Web.

Amphion has also been used in the study of the various phases of the Moon and Mars. Click on the link below to see an explanation.

Phases of the Heavenly Bodies

Reviewed 2012


NASA Researchers

Past NASA Researchers

  • Santos Lazzeri
  • Andrew Philpot
  • Arthur Reyes
  • Steven Roach
  • Grigore Rosu
  • Ian Underwood
  • Jeffrey Van Baalen

Other Info


First Gov logo
NASA Logo -