Formal analysis of a space-craft controller using SPIN

This paper documents an application of the finite state model checker SPIN to formally analyze a multithreaded plan execution module, The plan executi on module is one component of NASA's New Millennium Remote Agent, an artifi cial intelligence-based space-craft control system architecture which launc hed in October of 1998 as part of the DEEP SPACE 1 mission. The bottom laye r of the plan execution module architecture is a domain specific language, named ESL (Executive Support Language), implemented as an extension to mult ithreaded COMMON LISP. ESL supports the construction of reactive control me chanisms for autonomous robots and space-craft, For this case study, we tra nslated the ESL services for managing interacting parallel goal-and-event d riven processes into the PROMELA input language of SPIN, A total of five pr eviously undiscovered concurrency errors were identified within the impleme ntation of ESL. According to the Remote Agent programming team, the effort has had a major impact, locating errors that would not have been located ot herwise and, in one case, identifying a major design flaw. In fact, in a di fferent part of the system, a concurrency bug identical to one discovered b y this study escaped testing and caused a deadlock during an in-flight expe riment 96 million kilometers from earth. The work additionally motivated th e introduction of procedural abstraction in terms of inline procedures into SPIN.