NASA Logo, National Aeronautics and Space Administration

Remote Agent Executive for Deep Space 1

1999 Co-Winner of NASA's Software of the Year Award

The paper listed below describes an application of the finite state model checker SPIN to formally verify a multi-threaded plan execution programming language. The plan execution language is one component of NASA's New Millennium Remote Agent, an artificial intelligence based spacecraft control system architecture that is scheduled to launch in October of 1998 as part of the DEEP SPACE 1 mission to Mars. The language is concretely named ESL (Executive Support Language) and is basically a language designed to support the construction of reactive control mechanisms for autonomous robots and space crafts. It offers advanced control constructs for managing interacting parallel goal-and- event driven processes, and is currently implemented as an extension to a multi-threaded COMMON LISP. A total of errors were in fact identified, of which were important. This is regarded as a very successful result. According to the Remote Agent programming team the effort has had a major impact, locating errors that would probably not have been located otherwise and identifying a major design flaw. The work additionally motivated the introduction of procedural abstraction in terms of inline procedures in SPIN.

References

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN," Proc. SPIN'98: 4th Int'l SPIN Workshop, volume 27, issue 8, Paris, France, pp. 749-765, Nov. 2, 1998.
[papers (PDF, 148K),(PostScript, 225K)]

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN," (modified), IEEE Transactions on Software Engineering, vol. 27, no. 8, pp. 749-765, Aug. 2001.
[papers (PDF,165K),(Postscript, 209K)]

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN," (extended version), NASA Ames Tech. Report, no. 1770, Nov. 1997.
[tech reports (PDF, 443K),(PostScript, 666K)]

Reviewed 2012

First Gov logo
NASA Logo - nasa.gov