Abstract
This paper discusses the verification and validation (V&V) of advanced software used for integrated vehicle health monitoring (IVHM), in the context of NASA’s next-generation space shuttle. We survey the current V&V practice and standards used in selected NASA projects, review applicable formal verification techniques, and discuss their integration into existing development practice and standards. We also describe two verification tools, JMPL2SMV and Livingstone PathFinder, that can be used to thoroughly verify diagnosis applications that use model-based reasoning, such as the Livingstone system.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L.: Philippe Schnoebelen with Pierre McKenzie. Systems and Software Verification Model-Checking Techniques and Tools. Springer, Heidelberg (1998)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Costello, K.: Private communication. NASA IV&V Facility, October 13 (2001)
Feather, M.S.: Rapid Application of Lightweight Formal Methods for Consistency Analyses. IEEE Transactions on Software Engineering 24(11), 949–959 (1998)
Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.L.: Formal Analysis of the Remote Agent Before and After Flight. In: Proceedings of 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, June 13-15 (2000)
Havelund, K., Pressburger, T.: Model Checking Java Programs Using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2(4) (April 2000)
Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathFinder. In: First Workshop on Runtime Verification (RV 2001), Paris, France. Electronic Notes in Theoretical Computer Science, vol. 55(2), July 23 (2001)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5) (May 1997)
IEEE/EIA. Industry Implementation of International Standard ISO/IEC: ISO/IEC12207 Standard for Information Technology—Software life cycle processes. IEEE/EIA 12207.0-1996
IEEE/EIA. Industry Implementation of International Standard ISO/IEC: ISO/IEC12207 Standard for Information Technology—Software life cycle processes—Life cycle data. IEEE/EIA 12207.1-1997
IEEE/EIA. Industry Implementation of International Standard ISO/IEC: ISO/IEC12207 Standard for Information Technology—Software life cycle processes—Implementation Considerations. IEEE/EIA 12207.2-1997
Muscettola, N., Nayak, P.P., Pell, B., Williams, B.: Remote Agent: To boldly go where no AI system has gone before. Artificial Intelligence 103(1-2), 5–48 (1998)
NASA. NASA Software Guidelines and Requirements. NASA NPG 2820.DRAFT, 3/19/01
NASA. Software Independent Verification and Validation (IV&V) Management. NASA NPG 8730.DRAFT 2 (Novemeber 30, 2001)
Nelson, S., Pecheur, C.: NASA processes/methods applicable to IVHM V&V. Project report, NASA/CR-2002-211401 (April 2002)
Nelson, S., Pecheur, C.: Methods for V&V of IVHM intelligent systems. Project report, NASA/CR-2002-211402 (April 2002)
Nelson, S., Pecheur, C.: Diagnostic Model V&V Plan/Methods for DME. Project report, NASA/CR-2002-211403 (April 2002)
Grumman, N.: ASA, DSI. In: Brown, S.A. (ed.) 2nd Generation RLV Risk Reduction Program: TA-5 (IVHM) Project Notebook, Northrop Grumman, El Segundo, CA, July 20 (2001)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Pecheur, C., Cimatti, A.: Formal Verification of Diagnosability via Symbolic Model Checking. In: Workshop on Model Checking and Artificial Intelligence (Mo-ChArt 2002), Lyon, France, July 22-23 (2002)
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)
PolySpace Technologies. C Verifier, http://www.polyspace.com
RTCA. Software Considerations in Airborne Systems and Equipment Certification. RTCA (Requirements and Technical Concepts for Aviation) /DO-178B, December 1 (1992)
Rushby, J.: Assurance for Dependable Systems (Disappearing Formal Methods). Presentation at Safecomp, Budapest (September 2001), TU Vienna (March 2001), NSA (March 2001)
Williams, B.C., Nayak, P.P.: A model-based approach to reactive self-configuring systems. In: Proceedings of AAAI 1996 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nelson, S.D., Pecheur, C. (2003). Formal Verification for a Next-Generation Space Shuttle. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C., Gordon-Spears, D. (eds) Formal Approaches to Agent-Based Systems. FAABS 2002. Lecture Notes in Computer Science(), vol 2699. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45133-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-45133-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40665-5
Online ISBN: 978-3-540-45133-4
eBook Packages: Springer Book Archive