Amphion/NAV: Deductive Synthesis of State Estimation Software
Abstract
Previous work on domain-specific deductive program synthesis described the Amphion/NAIF system for generating Fortran code from high-level graphical specifications describing problems in space system geometry. Amphion/NAIF specifications describe input-output functions that compute geometric quantities (e.g., the distance between two planets at a point in time, or the time when a radio communication path between a spacecraft and earth is occluded) by composing together Fortran subroutines from the NAIF subroutine library developed at the Jet Propulsion Laboratory. In essence, Amphion/NAIF synthesizes code for glueing together the NAIF components in a way such that the generated code implements the specification, with a concurrently generated proof that this implementation is correct. Amphion/NAIF demonstrated the success of domain-specific deductive program synthesis and is still in use today within the space science community. However, a number of questions remained open that we will attempt to answer in this paper.
BibTeX
@inproceedings{Whittle-al:ASE01,
author = {Jon Whittle and
Jeffrey Van Baalen and
Johann Schumann and
Peter Robinson and
Thomas Pressburger and
John Penix and
Phil Oh and
Michael R. Lowry and
Guillaume P. Brat},
title = {{Amphion/NAV:} Deductive Synthesis of State Estimation Software},
booktitle = {ASE},
pages = {395--399},
publisher = {{IEEE} Computer Society},
year = {2001},
}