Issue No.08 - August (2001 vol.27)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.940728
<p><b>Abstract</b>—This paper documents an application of the finite state model checker S<scp>pin</scp> 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 space-craft control system architecture which launched in October of 1998 as part of the D<scp>eep</scp> S<scp>pace</scp> 1 mission. The bottom layer of the plan execution module architecture is a domain specific language, named E<scp>sl</scp> (Executive Support Language), implemented as an extension to multithreaded C<scp>ommon</scp> L<scp>isp</scp>. E<scp>sl</scp> supports the construction of reactive control mechanisms for autonomous robots and space-craft. For this case study, we translated the E<scp>sl</scp> services for managing interacting parallel goal-and-event driven processes into the P<scp>romela</scp> input language of S<scp>pin</scp>. A total of five previously undiscovered concurrency errors were identified within the implementation of E<scp>sl</scp>. According to the Remote Agent programming team, the effort has had a major impact, locating errors that would not have been located otherwise and, in one case, identifying a major design flaw. In fact, in a different part of the system, a concurrency bug identical to one discovered by this study escaped testing and caused a deadlock during an in-flight experiment 96 million kilometers from earth. The work additionally motivated the introduction of procedural abstraction in terms of inline procedures into S<scp>pin</scp>.</p>
Program verification, concurrent programs, model checking, temporal logic, program abstraction, model extraction, space-craft software.
Klaus Havelund, Mike Lowry, John Penix, "Formal Analysis of a Space-Craft Controller Using SPIN", IEEE Transactions on Software Engineering, vol.27, no. 8, pp. 749-765, August 2001, doi:10.1109/32.940728