Formal analysis of a space-craft controller using SPIN.

The paper documents an application of the finite state model checker SPIN to formally analyze a multithreaded plan execution module. The plan execution module is one component of NASA's New Millennium Remote Agent, an artificial intelligence-based spacecraft control system architecture which la...

Full description

Bibliographic Details
Published in:	IEEE Transactions on software engineering 27, 8 (2001).
Main Author:	Havelund, K.
Format:	Article
Language:	English
Subjects:	DEEP SPACE 1 mission. ESL services. Executive Support Language. New Millennium Remote Agent. PROMELA input language. Remote Agent programming team. SPIN. Artificial intelligence-based spacecraft control system architecture. Autonomous robots. Concurrency bug. Concurrency errors. Design flaw. Domain specific language. Finite state model checker. Formal analysis. In-flight experiment. Inline procedures. Interacting parallel goal-and-event driven processes. Multithreaded COMMON LISP. Multithreaded plan execution module. Plan execution module architecture. Procedural abstraction. Reactive control mechanisms. Spacecraft controller.