Abstract
AI software is often used as a means for providing greater autonomy to automated systems, capable of coping with harsh and unpredictable environments. Due in part to the enormous space of possible situations that they aim to address, autonomous systems pose a serious challenge to traditional test-based verification approaches. Efficient verification approaches need to be perfected before these systems can reliably control critical applications. This publication describes Livingstone PathFinder (LPF), a verification tool for autonomous control software. LPF applies state space exploration algorithms to an instrumented testbed, consisting of the controller embedded in a simulated operating environment. Although LPF has focused on NASA’s Livingstone model-based diagnosis system applications, the architecture is modular and adaptable to other systems. This article presents different facets of LPF and experimental results from applying the software to a Livingstone model of the main propulsion feed subsystem for a prototype space vehicle.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bajwa, A., Sweet, A.: The Livingstone Model of a Main Propulsion System. In: Proceedings of the IEEE Aerospace Conference (March 2003)
Brinksma, E.: A Theory for the Derivation of Tests. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing and Verification, vol. VIII, pp. 63–74. North-Holland, Amsterdam (1988) ISBN 0-444-70542-2
Fleming, L., Hatfield, T., Malin, J.: Simulation-Based Test of Gas Transfer Control Software: CONFIG Model of Product Gas Transfer System. Automation, Robotics and Simulation Division Report, AR&SD-98-017, NASA Johnson Space Center Center, Houston, TX (1998)
Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, Paris, January 1997, pp. 174–186 (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Lindsey, A.E., Pecheur, C.: Simulation-Based Verification of Livingstone Applications. In: Workshop on Model-Checking for Dependable Software-Intensive Systems, San Francisco (June 2003)
Muscettola, N., Nayak, P., Pell, B., Williams, B.: Remote Agent: To Boldly Go Where No AI System Has Gone Before. Artificial Intelligence 103, 5–47 (1998)
Meyer, C., Cannon, H.: Propulsion IVHM Technology Experiment Overview. In: Proceedings of the IEEE Aerospace Conference, March 8-15 (2003)
Pecheur, C., Simmons, R.: From Livingstone to SMV: Formal Verification for Autonomous Spacecrafts. In: Rash, J.L., Rouff, C.A., Truszkowski, W., Gordon, D.F., Hinchey, M.G. (eds.) FAABS 2000. LNCS (LNAI), vol. 1871, p. 103. Springer, Heidelberg (2001)
Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proceedings of the IEEE International Conference on Automated Software Engineering, September 2000, pp. 3–12 (2000)
Williams, B., Ingham, M., Chung, S., Elliot, P.: Model-based Programming of Intelligent Embedded Systems and Robotic Space Explorers. In: Proceedings of the IEEE Modelings and Design of Embedded Software Conference, vol. 9(1), pp. 212–237 (2003)
Williams, B., Nayak, P.: A Model-based Approach to Reactive Self-Configuring Systems. In: Proceedings of the National Conference on Artificial Intelligence, vol. 2, pp. 971–978 (August 1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lindsey, A.E., Pecheur, C. (2004). Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive