Judith Crow
Abstract
This article describes four case studies in which requirements for new flight software subsystems on NASA's Space Shuttle were analyzed using mechanically supported formal methods. Three of the studies used standard formal specification and verification techniques, and the fourth used state exploration. These applications illustrate two thesis: (1) formal methods complement conventional requirements analysis processes effectively and (2) formal methods confer benefits even when only selectively adopted and applied. The studies also illustrate the interplay of application maturity level and formal methods strategy, especially in areas such as technology transfer, legacy applications, and rapid formalization, and they raise interesting issues in problem domain modeling and in tailoring formal techniques to applications.
- AGERHOLM, S. AND LARSEN, P. G. 1997. Modeling and validating SAFER in VDM-SL. In Proceedings of the 4th NASA Langley Formal Methods Workshop (LFM '97) (Hampton, VA, Sept.), C. M. Holloway and K. J. Hayhurst, Eds. NASA Langley Research Center, Hampton, VA, 51-64. Available via http://atb-www.larc.nasa.gov/lfm97/proceedings.Google Scholar
- ALUR, R. AND HENZINGER, T. A., EDS. 1996. Computer-Aided Verification (CAV '96) (New Brunswick, NJ, July-Aug.). Lecture Notes in Computer Science, vol. 1102. Springer- Verlag, New York, NY. Google Scholar
- BROCK, B., KAUFMANN, M., AND MOORE, J. S. 1996. ACL2 theorems about commercial microprocessors. In Formal Methods in Computer-Aided Design (FMCAD '96) (Palo Alto, CA, Nov.), M. Srivas and A. Camilleri, Eds. Lecture Notes in Computer Science, vol. 1166. Springer-Verlag, New York, NY, 275-293. Google Scholar
- BROOKES, T., FITZGERALD, J., AND LARSEN, P. 1996. Formal and informal specification of a secure system component: Final results in a comparative study. In Formal Methods Europe (FME '96) (Oxford, England, Mar.). Lecture Notes in Computer Science, vol. 1051. Springer- Verlag, New York, NY, 214-227. Google Scholar
- BUTLER, R. W., CALDWELL, J. L., CARRE O, V. A., HOLLOWAY, C. M., MINER, P. S., AND DI VITO, B.L. 1995. NASA Langley's research and technology transfer program in formal methods. In Proceedings of the l Oth Annual Conference on Computer Assurance (COMPASS '95) (Gaithersburg, MD, June 1995), 135-149.Google Scholar
- CLARKE, E. M., GERMAN, S. M., AND ZHAO, X. 1996a. Verifying the SRT division algorithm using theorem proving techniques. In Computer-Aided Verification (CAV '96) (New Brunswick, NJ, July/Aug.), R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, NY, 111-122. Google Scholar
- CLARKE, E., WING, J. M., ALUR, R., CLEAVELAND, R., DILL, D., EMERSON, A., GARLAND, S., GERMAN, S., GUTTAG, J., HALL, A., HENZINGER, T., HOLZMANN, G., JONES, C., KURSHAN, R., LEVESON, N., MCMILLAN, K., MOORE, J., PELED, D., PNUELI, A., RUSHBY, J., SHANKAR, N., SIFAKIS, J., SISTLA, P., STEFFEN, B., WOLPER, P., WOODCOCK, J., AND ZAVE, P. 1996b. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4 (Dec.), 626-643. Google Scholar
- CRAIGEN, D., GERHART, S., AND RALSTON, T. 1993a. An international survey of industrial applications of formal methods. Vol. 1, Purpose, approach, analysis and conclusions. Tech. Rep. NIST GCR 93/626. National Institute of Standards and Technology, Gaithersburg, MD.Google Scholar
- CRAIGEN, D., GERHART, S., AND RALSTON, T. 1993b. An international survey of industrial applications of formal methods. Vol. 2, Case studies. Tech. Rep. NIST GCR 93/626. National Institute of Standards and Technology, Gaithersburg, MD.Google Scholar
- CROW, J. 1995. Finite-state analysis of space shuttle contingency guidance requirements. Tech. Rep. SRI-CSL-95-17, Computer Science Laboratory, SRI International, Menlo Park, CA. Also available as Contractor Rep. 4741, NASA Langley Research Center, Hampton, VA, May 1996. Google Scholar
- CURZON, P. 1994. The formal verification of the Fairisle ATM switching element: An overview. Tech. Rep. 328, Univ. of Cambridge Computer Laboratory, Cambridge, UK. Available via http://www.cl.cam.ac.uk/users/pc/elltr94.htmlGoogle Scholar
- DI VITO, B. L. 1996. Formalizing new navigation requirements for NASA's space shuttle. In Formal Methods Europe (FME '96) (Oxford, England, Mar.). Lecture Notes in Computer Science, vol. 1051. Springer-Verlag, New York, NY, 160-178. Google Scholar
- DI VITO, B. L. AND ROBERTS, L.W. 1996. Using formal methods to assist in the requirements analysis of the space shuttle GPS change request. Contractor Rep. 4752, NASA Langley Research Center, Hampton, VA. Google Scholar
- DILL, D.L. 1996. The Mur4~ verification system. In Computer-Aided Verification (CAV '96) (New Brunswick, NJ, July/Aug.), R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, NY, 390-393. Google Scholar
- DILL, D. L., DREXLER, A. J., Hu, A. J., AND YANG, C. H. 1992. Protocol verification as a hardware design aid. In Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors (Cambridge, MA, Oct. 11-14). IEEE Computer Society, Washington, DC, 522-525. Google Scholar
- DUTERTRE, B. AND STAVRIDOU, V. 1997. Formal requirements analysis of an avionics control system. IEEE Trans. Softw. Eng. 23, 5 (May), 267-278. Google Scholar
- HAMILTON, D., COVINGTON, R., AND KELLY, J. 1995a. Experiences in applying formal methods to the analysis of software and system requirements. In Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques (WIFT '95) (Boca Raton, FL). IEEE Computer Society, Washington, DC, 30-43. Google Scholar
- HAMILTON, D., COVINGTON, R., AND LEE, n. 1995b. Experience report on requirements reliability engineering using formal methods. In Proceedings of the International Conference on Software Reliability Engineering (ISSRE '95) (Toulouse, France). IEEE Computer Society, Washington, DC.Google Scholar
- HAVELUND, K. AND SHANKAR, N. 1996. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe (FME '96) (Oxford, England, Mar.). Lecture Notes in Computer Science, vol. 1051. Springer-Verlag, New York, NY, 662-681. Google Scholar
- HEIMDAHL, M. P. E. AND LEVESON, N.G. 1996. Completeness and consistency in hierarchical state-based requirements. IEEE Trans. Softw. Eng. 22, 6 (June), 363-377. Google Scholar
- HENINGER, K. L. 1980. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. Softw. Eng. SE-6, 1 (Jan.), 2-13.Google Scholar
- HINCHEY, M. G. AND BOWEN, J. P., EDS. 1995. Applications of Formal Methods. Prentice- Hall International Series in Computer Science. Prentice Hall International (UK) Ltd., Hertfordshire, UK. Google Scholar
- HINCHEY, M. G. AND BOWEN, g. P., EDS. 1997. Industrial Strength Formal Methods. Academic Press, Inc., Orlando, FL. Google Scholar
- IP, C. N. AND DILL, D.L. 1993. Better verification through symmetry. In Proceedings of the 11th Conference on Computer Hardware Description Languages and Their Applications (CHDL '93). International Federation for Information Processing, Laxenburg, Austria, 87-100. Google Scholar
- JACKY, J. 1995. Specifying a safety-critical control system in Z. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 99-106. Google Scholar
- KROPF, T., ED. 1997. Formal Hardware Verification: Methods and Systems in Comparison. Springer Lecture Notes in Computer Science, vol. 1287. Springer-Verlag, New York, NY. Google Scholar
- LADKIN, P.B. 1995. Analysis of a technical description of the airbus A320 braking system. High Integrity Syst. 1, 4, 331-349.Google Scholar
- LUTZ, R. R. AND AMPO, Y. 1994. Experience report: Using formal methods for requirements analysis of critical spacecraft software. In Proceedings of the 19th Annual Software Engineering Workshop. NASA GSFC, Greenbelt, MD, 231-248.Google Scholar
- MOORE, J. S., LYNCH, T., AND KAUFMANN, M. 1996. A mechanically checked proof of the correctness of the AMD5k86 floating-point division algorithm. Tech. Rep. Available via http://devil.ece.utexas.edu:80/-lynch/divide/divide_paper.psGoogle Scholar
- NASA. 1993. Formal methods demonstration project for space applications--Phase I case study: Space Shuttle orbit DAP jet select. NASA Code Q Final Rep (Unnumbered), National Aeronautics and Space Administration, Washington, DC. Jet Select requirements specification appears as Appendix B.Google Scholar
- NRCC. 1993. An Assessment of Space Shuttle Flight Software Development Practices. National Academy Press, Washington, DC. Google Scholar
- OWRE, S., RUSHBY, J., SHANKAR, N., AND VON HENKE, F. 1995. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21, 2 (Feb.), 107-125. Google Scholar
- OWRE, S., SHANKAR, N., AND RUSHBY, J.M. 1993a. User Guide for the PVS Specification and Verification System. Vol. 1, Language Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA.Google Scholar
- OWRE, S., SHANKAR, N., AND RUSHBY, J.M. 1993b. User Guide for the PVS Specification and Verification System. Vol. 2, System Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA.Google Scholar
- OWRE, S., SHANKAR, N., AND RUSHBY, J.M. 1993c. User Guide for the PVS Specification and Verification System. Vol. 3, Prover Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA.Google Scholar
- PARNAS, D.L. 1995. Using mathematical models in the inspection of critical software. In Applications of Formal Methods, M. G. Hinchey and J. P. Bowen, Eds. Prentice-Hall International Series in Computer Science. Prentice Hall International (UK) Ltd., Hertfordshire, UK, 17-31.Google Scholar
- ROBERTS, L. W. AND BEIMS, M. 1996. Using formal methods to assist in the requirements analysis of the space shuttle HAC change request (CR90960E). JSC Tech. Rep. Loral Space Information Systems, Houston, TX. Google Scholar
- RUSHBY, J. 1996. Automated deduction and formal methods. In Computer-Aided Verification (CAV '96) (New Brunswick, NJ, July/Aug.), R. Alur and T. A. Henzinger, Eds. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, NY, 169-183. Google Scholar
- SCHNEIDER, F., EASTERBROOK, S., CALLAHAN, J., AND HOLZMANN, G. 1998. Validating requirements for fault tolerant systems using model checking. In Proceedings of the 3rd International Conference on Requirements Engineering (ICRE '98). IEEE Computer Society, Washington, DC. Google Scholar
- SREEMANI, T. AND ATLEE, J.M. 1996. Feasibility of model checking software requirements. In Proceedings of the 11th Annual Conference on Computer Assurance (Gaithersburg, MD, June). IEEE Computer Society, Washington, DC, 77-88.Google Scholar
- SRIVAS, M. K. AND MILLER, S. P. 1995. Formal verification of the AAMP5 microprocessor. In Applications of Formal Methods, M. G. Hinchey and J. P. Bowen, Eds. Prentice-Hall International Series in Computer Science. Prentice Hall International (UK) Ltd., Hertfordshire, UK, 125-180. Google Scholar
- SRIVAS, M. K. AND MILLER, S.P. 1996. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods Syst. Des. 8, 2, 153-188. Google Scholar
- VAN SCHOUWEN, A. J. 1990. The A-7 requirements model: Re-examination for real-time systems and an application to monitoring systems. Tech. Rep. 90-276, Dept. of Computing and Information Science. Queen's University, Kingston, Ontario, Canada.Google Scholar
Index Terms
- Formalizing space shuttle software requirements: four case studies
Recommendations
A user-friendly formal requirements specification method
ACM-SE 30: Proceedings of the 30th annual Southeast regional conferenceAs formal methods are increasingly used in the development of industrial scale software systems, there is a growing awareness of the need to integrate the formal notations with existing structured software development methods. In order to make ...
Using the Base Semantics given by fUML for Verification
MODELSWARD 2014: Proceedings of the 2nd International Conference on Model-Driven Engineering and Software DevelopmentThe lack of formal foundations in the UML results in imprecise models, since UML defines the graphical notations and an abstract syntax for them, but not their formal semantics. Semantics for the key parts of activities and classes is defined by the ...
Reviews
Mauro Pezze
A set of coordinated experiments studied the application of formal methods to space shuttle software requirements specifications. This paper describes the application of different formal methods (theorem proving and reachability analysis) using different tools (PVS and Mur(PHI)) to a set of shuttle software systems. It explores and documents the feasibility and utility of formalizing critical shuttle software requirements. The authors discuss the development of reusable formal methods strategies for representative classes of shuttle software. They identify and assess key factors in the transfer of this technology to the aerospace community. They then compare the formal methods across a range of maturity levels of software requirements. Most of the results presented in the paper will not surprise formal methods experts. However, the size of the experiments, the variety of software considered, and the detailed description of the results provide important experimental data for formal methods experts, as well as for practitioners. The authors also identify several methodological guidelines that may greatly help in transferring this technology not only to the shuttle program, but to many other application domains. The requirement specifications considered are the GPS retrofit system, which elaborates GPS data; the JS system, responsible for the selection of the shuttle's Reaction Control System Jets; the Heading Alignment Cylinder (HAC), responsible for tuning important navigation data; and the 3E/O system, which monitors ascending parameters. The size of the analyzed specifications ranges from 20 pages of tables, diagrams, and informal description for the HAC software to 110 pages for the GPS software. The GPS, JS, and HAC software are specified and analyzed using PVS, while the 3E/O system is specified and analyzed using Mur(PHI). The analysis ranges from identification of problems while specifying the system (GPS) to theorem proving (JS and HAC) and reachability analysis (3E/O). The paper clearly demonstrates the utility of formal methods as a complement to the conventional shuttle requirements analysis process. In all cases, formal specifications were obtained without much effort, the formal specifications were much smaller than the informal ones (from 200 to 3300 PVS lines ), and the method uncovered anomalies ranging from annoyance to critical errors. These anomalies would have been revealed using the conventional analysis process, but that would have been more expensive and time-consuming. The paper isolates the minimum set of required technical details from the presentation and analysis of the actual data produced from the experiments and the conclusions. It can be easily read by formal methods experts as well as practitioners; the results will interest both of these audiences.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments