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...

Descripción completa

Detalles Bibliográficos
Publicado en:	IEEE Transactions on software engineering 27, 8 (2001).
Autor principal:	Havelund, K.
Formato:	Artículo
Lenguaje:	English
Materias:	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.