This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Analysis of a Space-Craft Controller Using SPIN
August 2001 (vol. 27 no. 8)
pp. 749-765

Abstract—This 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 space-craft control system architecture which launched in October of 1998 as part of the Deep Space 1 mission. The bottom layer of the plan execution module architecture is a domain specific language, named Esl (Executive Support Language), implemented as an extension to multithreaded Common Lisp. Esl supports the construction of reactive control mechanisms for autonomous robots and space-craft. For this case study, we translated the Esl services for managing interacting parallel goal-and-event driven processes into the Promela input language of Spin. A total of five previously undiscovered concurrency errors were identified within the implementation of Esl. 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 Spin.

[1] S. Bensalem, Y. Lakhnech, and S. Owre, “Computing Abstractions of Infinite State Systems Compositionally and Automatically,” Proc. CAV '98: Computer-Aided Verification, 1998.
[2] S. Bensalem, Y. Lakhnech, and S. Owre, “InVeSt: A Tool for the Verification of Invariants,” Proc. CAV '98: Computer-Aided Verification, 1998.
[3] J.C. Corbett, “Constructing Compact Models of Concurrent Java Programs,” Proc. ACM Int'l Symp. Software Testing and Analysis (ISSTA'98), pp. 1-10, 1998.
[4] C. Demartini, R. Iosif, and R. Sisto, “Modeling and Validation of Java Multithreading Applications Using SPIN,” Proc. Fourth SPIN Workshop, Nov. 1998.
[5] S. Graf and H. Saidi, “Construction of Abstract State Graphs with PVS,” Proc. CAV '97: Computer-Aided Verification, 1997.
[6] K. Havelund and T. Pressburger, “Model Checking Java Programs using Java PathFinder,” Int'l J. Software Tools for Technology Transfer (STTT), vol. 2, no. 4, pp. 366–381, Apr. 2000.
[7] K. Havelund and N. Shankar, "Experiments in Theorem Proving and Model Checking for Protocol Verification," Proc. Formal Methods Europe (FME'96), pp. 662-681, Lecture Notes in Computer Science 1051, Springer-Verlag, Mar. 1996.
[8] K. Havelund and J. Skakkebæk, “Applying Model Checking in Java Verification,” Theoretical and Practical Aspects of SPIN Model Checking—Proc. Fifth and Sixth Int'l SPIN Workshops, D. Dams, R. Gerth, S. Leue, and M. Massink, eds., July/Sept. 1999.
[9] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[10] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas, "PVS: Combining Specification, Proof Checking, and Model Checking," Alur and Henzinger [4], pp. 411-414.
[11] B. Pell, E. Gat, R. Keesing, N. Muscettola, and B. Smith, “Plan Execution for Autonomous Spacecrafts,” Proc. Int'l Joint Conf. AI, Aug. 1997.
[12] G.L. Steele, Common Lisp: The Language, second ed. Digital Press, 1990.

Index Terms:
Program verification, concurrent programs, model checking, temporal logic, program abstraction, model extraction, space-craft software.
Citation:
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, Aug. 2001, doi:10.1109/32.940728
Usage of this product signifies your acceptance of the Terms of Use.