This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Experiences Using Lightweight Formal Methods for Requirements Modeling
January 1998 (vol. 24 no. 1)
pp. 4-14

Abstract—This paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process, to validate the evolving requirements. The results were fed back into the projects, to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes, by testing key properties of the evolving requirements, and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.

[1] N.G. Leveson, Safeware: System Safety and Computers. Addison-Wesley, 1995.
[2] B.W. Boehm, Software Eng. Economics.Englewood Cliffs, N.J.: Prentice Hall, 1981.
[3] R. Lutz, "Analyzing Software Requirements Errors in Safety-Critical, Embedded Systems," Proc. IEEE Int'l Symp. Requirements Eng., RE '93, pp. 126-133,San Diego, Calif., Jan. 1993.
[4] J.C. Kelly, J.S. Sherif, and J. Hops, "An Analysis of Defect Densities Found During Software Inspections," J. Systems Software, Feb. 1992, pp. 111-117.
[5] J. Crow, "Finite-State Analysis of Space Shuttle Contingency Guidance Requirements," Technical Report SRI-CSL-95-17, Computer Science Laboratory, SRI International, Menlo Park, Calif., 1995.
[6] J. Crow and B.L. Di Vito, "Formalizing Space Shuttle Software Requirements," Workshop Formal Methods in Software Practice (FMSP '96),San Diego, Calif., Jan. 1996.
[7] B.L. Di Vito, "Formalizing New Navigation Requirements for NASA's Space Shuttle," Proc. Formal Methods Europe (FME '96),Oxford, England, Mar. 1996.
[8] J.L. Lions, "ARIANE 5 Flight 501 Failure: Report by the Enquiry Board," European Space Agency, Paris 1996.
[9] J. Rushby, "Formal Methods and Their Role in the Certification of Critical Systems," Technical Report CSL-95-1, Computer Science Laboratory, SRI International, Menlo Park, Calif., 1995.
[10] A. Finkelstein et al., "Inconsistency Handling in Multi-Perspective Specifications," IEEE Trans. Software Eng., vol. 20, no. 8, Aug. 1994, pp. 569-578.
[11] D. Hamilton, R. Covington, and J.C. Kelly, "Experiences in Applying Formal Methods to the Analysis of Software and System Requirements," Proc. IEEE Workshop Industrial-Strength Formal Specification Techniques (WIFT '95),Boca Raton, Fla., Apr. 1995.
[12] R.W. Butler, J.L. Caldwell, V.A. Carreno, C.M. Holloway, P.S. Miner, and B.L. Di Vito, "NASA Langley's Research and Technology Transfer Program in Formal Methods," Proc. 10th Ann. Conf. Computer Assurance (COMPASS 95),Gaithersburg, Md., June 1995.
[13] D. Hamilton, R. Covington, and A. Lee, "An Experience Report on Requirements Reliability Engineering Using Formal Methods," IEEE Int'l Conf. Software Reliability Eng.,France, Oct. 1995.
[14] S. Easterbrook and J. Callahan, "Formal Methods for V&V of Partial Specifications: An Experience Report," Proc., Third IEEE Symp. Requirements Eng. (RE'97),Annapolis, Md., Jan. 1997.
[15] Y. Ampo and R.R. Lutz, "Evaluation of Software Safety Analysis using Formal Methods," Proc. Foundation of Software Eng. '95,Hamana-ko, Japan, Dec. 1995.
[16] NASA, "Formal Methods Specification and Verification Guidebook for Software and Computer Systems. Vol. 1: Planning and Technology Insertion," Report NASA-GB-002-95, NASA Office of Safety and Mission Assurance, Washington D.C., 1995.
[17] NASA, "Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems. Vol. 2: A Practitioner's Companion," Report NASA-GB-001-97, NASA Office of Safety and Mission Assurance, Washington D.C., 1997.
[18] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107-125, Feb. 1995.
[19] C.L. Heitmeyer, B.L. Labaw, and D. Kiskis, "Consistency Checking of SCR-style Requirements Specifications," Proc. Int'l Symp. Requirements Engineering, Mar. 1995.
[20] M.P. Heimdahl and N.G. Leveson, "Completeness and Consistency in Hierarchical State-Based Requirements," IEEE Trans. Software Eng., pp. 363-377, vol. 22, June 1996.
[21] C.L. Chang, R.A. Stachowitz, and J.B. Combs, “Validation of Nonmonotonic Knowledge-Based Systems,” Proc. IEEE Int'l Conf. Tools for Artificial Intelligence, Nov. 1990.
[22] S. Easterbrook and J. Callahan, "Independent Validation of Specifications: A Coordination Headache," Proc., IEEE Fifth Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE'96),Stanford, Calif., June 1996.
[23] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[24] A. Hall, “Using Formal Methods to Develop an ATC Information System,” IEEE Software, vol. 13, no. 2, pp. 66–76, Mar. 1996.
[25] D. Craigen, S. Gerhart, and T. Ralston, “Formal Methods Reality Check: Industrial Usage,” IEEE Trans. Software Eng., vol. 21, no. 2, pp. 90–98, Feb. 1995.
[26] R.A. Kemmerer, "Integrating Formal Methods into the Development Process," IEEE Software, vol. 7, pp. 37-50, 1990.
[27] P.G. Larsen, J. Fitzgerald, and T. Brookes, "Applying Formal Specifications in Industry," IEEE Software, vol. 13, no. 5, May 1996, pp. 48-56.

Index Terms:
Software requirements, formal methods, verification and validation, fault protection software, NASA.
Citation:
Steve Easterbrook, Robyn Lutz, Richard Covington, John Kelly, Yoko Ampo, David Hamilton, "Experiences Using Lightweight Formal Methods for Requirements Modeling," IEEE Transactions on Software Engineering, vol. 24, no. 1, pp. 4-14, Jan. 1998, doi:10.1109/32.663994
Usage of this product signifies your acceptance of the Terms of Use.