Abstract
We describe a recent NASA-sponsored pilot project intended to gauge the effectiveness of using formal methods in Space Shuttle software requirements analysis. Several Change Requests (CRs) were selected as promising targets to demonstrate the utility of formal methods in this demanding application domain. A CR to add new navigation capabilities to the Shuttle, based on Global Positioning System (GPS) technology, is the focus of this industrial usage report. Portions of the GPS CR were modeled using the language of SRI's Prototype Verification System (PVS). During a limited analysis conducted on the formal specifications, numerous requirements issues were discovered. We present a summary of these encouraging results and conclusions we have drawn from the pilot project.
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
A. Arnold, M-C. Gaudel, and B. Marre. An Experiment on the Validation of a Specification by Heterogeneous Formal Means: The Transit Node. In 5th IFIP Working Conference on Dependable Computing for Critical Applications (DCCA-5), Champaign-Urbana, IL, 1995.
Ricky W. Butler, James L. Caldwell, Victor A. Carreno, C. Michael Holloway, Paul S. Miner, and Ben L. Di Vito. NASA Langley's Research and Technology Transfer Program in Formal Methods. In Tenth Annual Conference on Computer Assurance (COMPASS 95), pages 135–149, Gaithersburg, MD, June 1995.
Dan Craigen, Susan Gerhart, and Ted Ralston. An international survey of industrial applications of formal methods; Volume 1: Purpose, approach, analysis and conclusions; Volume 2: Case studies. Technical Report NIST GCR 93/626, National Institute of Standards and Technology, Gaithersburg, MD, April 1993.
Judy Crow. Finite-State Analysis of Space Shuttle Contingency Guidance Requirements. Technical Report SRI-CSL-95-17, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1995. Also forthcoming as a NASA Contractor Report for Task NAS1-20334.
Ben L. Di Vito and Larry Roberts. Using Formal Methods to Assist in the Requirements Analysis of the Space Shuttle GPS Change Request. Contractor report, NASA Langley Research Center, Hampton, VA, 1996. To appear.
David Hamilton, Rick Covington, and John Kelly. Experiences in Applying Formal Methods to the Analysis of Software and System Requirements. In WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, pages 30–43, Boca Raton, FL, 1995. IEEE Computer Society.
David Hamilton, Rick Covington, and Alice Lee. Experience Report on Requirements Reliability Engineering Using Formal Methods. In ISSRE '95: International Conference on Software Reliability Engineering, Toulouse, France, 1995. IEEE Computer Society.
K. L. Heninger. Specifying Software Requirements for Complex Systems: New Techniques and Their Application. IEEE Transactions on Software Engineering, SE-6(1):2–13, January 1980.
Robyn R. Lutz and Yoko Ampo. Experience Report: Using Formal Methods for Requirements Analysis of Critical Spacecraft Software. In 19th Annual Software Engineering Workshop, pages 231–248. NASA GSFC, 1994. Greenbelt, MD.
Multi-Center NASA Team from Jet Propulsion Laboratory, Johnson Space Center, and Langley Research Center. Formal Methods Demonstration Project for Space Applications — Phase I Case Study: Space Shuttle Orbit DAP Jet Select, December 1993. NASA Code Q Final Report (Unnumbered).
National Aeronautics and Space Administration, Office of Safety and Mission Assurance, Washington, DC. Formal Methods Specification and Verification Guidebook for Software and Computer Systems, Volume I: Planning and Technology Insertion, July 1995. NASA-GB-002-95.
National Research Council Committee for Review of Oversight Mechanisms for Space Shuttle Flight Software Processes, National Academy Press, Washington, DC. An Assessment of Space Shuttle Flight Software Development Practices, 1993.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
John Rushby. Formal Methods and the Certification of Critical Systems. Technical Report SRI-CSL-93-7, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993. Also issued under the title Formal Methods and Digital Systems Validation for Airborne Systems as NASA Contractor Report 4551, December 1993.
A. John van Schouwen. The A-7 Requirements Model: Re-Examination for Real-Time Systems and an Application to Monitoring Systems. Technical Report 90-276, Department of Computing and Information Science, Queen's University, Kingston, Ontario, Canada, May 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Di Vito, B.L. (1996). Formalizing new navigation requirements for NASA's Space Shuttle. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_86
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_86
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive