This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications
November 1998 (vol. 24 no. 11)
pp. 927-948

Abstract—Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (Software Cost Reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.

[1] T.A. Alspaugh, S.R. Faulk, K. Heninger Britton, R.A. Parker, D.L. Parnas, and J.E. Shore, "Software Requirements for the A-7E Aircraft," Technical Report NRL-9194, Naval Research Laboratory, Washington, D.C., 1992.
[2] R.J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," Proc. Fourth ACM SIGSOFT Symp. Foundations of Software Eng., Oct. 1996.
[3] M. Archer and C. Heitmeyer, "The Use of Model Checking and Abstraction in Analyzing Requirements Specifications: A Formal Foundation," Technical Report, Naval Research Laboratory, Washington, D.C., 1998. Draft.
[4] M. Archer, C. Heitmeyer, and S. Sims, "TAME: A PVS Interface to Simplify Proofs for Automata Models," Proc. User Interfaces for Theorem Provers,Eindhoven, Netherlands, Eindhoven Univ. technical report, Eindhoven Univ. of Tech nology, July 1998.
[5] J.M. Atlee and M.A. Buckley, "A Logic-Model Semantics for SCR Specifications," Proc. Int'l Symp. Software Testing and Analysis, Jan. 1996.
[6] J.M. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, Jan. 1993.
[7] G. Berry and G. Gonthier, "The ESTERELSynchronous Programming Language: Design, Semantics, Implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[8] R. Bharadwaj, "A Generalized Validity Checker," technical report, Naval Research Laboratory, Washington, D.C., 1996.
[9] R. Bharadwaj and C. Heitmeyer, "Model Checking Complete Requirements Specifications Using Abstraction," Technical Report NRL-7999, Naval Research Laboratory, Washington, D.C., Nov. 1997.
[10] R. Bharadwaj and C. Heitmeyer, "Verifying SCR Requirements Specifications Using State Exploration," Proc. First ACM SIGPLAN Workshop Automatic Analysis of Software, 1997.
[11] R. Bharadwaj and C. Heitmeyer, "Model Checking Complete Requirements Specifications Using Abstraction," Automated Software Eng. J., vol. 6, no. 1, Jan. 1999.
[12] B. Boehm, Software Engineering Economics, Prentice Hall, Upper Saddle River, N.J., 1981, pp. 533-535.
[13] W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," IEEE Trans. Software Eng., vol. 24, no. 7, July 1998.
[14] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[15] E. Clarke, O. Grumberg, and D. Long, "Model Checking and Abstraction," Proc., Principles of Programming Languages (POPL), 1994.
[16] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[17] E.M. Clarke and R.P. Kurshan, "Computer-Aided Verification," IEEE Spectrum, pp. 61-67, June 1996.
[18] P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints," Proc. Symp. Principles of Programming Languages, 1977.
[19] D. Dams, R. Gerth, and O. Grumberg, "Abstract Interpretation of Reactive Systems," ACM Trans. Program Language and Systems, pp. 111-149, 1997.
[20] A.J. Dill, D.L. Drexler, A.J. Hu, and C.H. Yang, “Protocol Verification as a Hardware Design Aid,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors, 1992.
[21] S. Easterbrook and J. Callahan, "Formal Methods for Verification and Validation of Partial Specifications: A Case Study," J. Systems and Software, 1997.
[22] S. Easterbrook, R. Lutz, R. Covington, Y. Ampo, and D. Hamilton, "Experiences Using Lightweight Formal Methods for Requirements Modeling," IEEE Trans. Software Eng., vol. 24, no. 1, Jan. 1998.
[23] R. Fairley, Software Eng. Concepts.New York: McGraw-Hill, 1985.
[24] S. Faulk et al., "The Core Method For Real-Time Requirements," IEEE Software, Sept. 1992, pp. 22-33.
[25] S.R. Faulk, L. Finneran, J. Kirby, Jr., S. Shah, and J. Sutton, "Experience Applying the CoRE Method to the Lockheed C-130J," Proc. Ninth Ann. Conf. Computer Assurance (COMPASS'94), pp. 3-8,Gaithersburg, Md., June 1994.
[26] P. Godefroid, "Using Partial Orders to Improve Automatic Verification Methods," Proc. Second Int'l Workshop Computer-Aided Verification, pp. 176-185, 1990.
[27] S. Graf, "Characterization of a Sequentially Consistent Memory and Verification of a Cache Memory by Abstraction," Proc. Computer Aided Verification, 1994.
[28] S. Graf and C. Loiseaux, "A Tool for Symbolic Program Verification and Abstraction," Proc. Computer Aided Verification, pp. 71-84, 1993.
[29] K. Havelund and N. Shankar, "Experiments in Theorem Proving and Model Checking for Protocol Verification," Proc. Formal Methods Europe (FME'96), pp. 662-681, Lecture Notes in Computer Science 1051, Springer-Verlag, Mar. 1996.
[30] 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.
[31] C. Heitmeyer, J. Kirby, Jr., and B. Labaw, "Applying the SCR Requirements Method to a Weapons Control Panel: An Experience Report," Proc. Second ACM Workshop Formal Methods in Software Practice (FMSP'98), 1998.
[32] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, "Automated Consistency Checking of Requirements Specifications," ACM Trans. Software Eng. and Methodology, pp. 231-261, vol. 5, July 1996.
[33] C. Heitmeyer, "On the Need for Practical Formal Methods," Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98),Lyngby, Denmark, Sept. 1998.
[34] C.L. Heitmeyer, A. Bull, C. Gasarch, and B.G. Labaw, “SCR*: A Toolset for Specifying and Analyzing Requirements,” Proc. Conf. Computer Assurance (COMPASS), pp. 109–122, June 1995.
[35] C. Heitmeyer, J. Kirby, Jr., and B. Labaw, "Tools for Formal Specification, Verification, and Validation of Requirements," Proc. 12th Ann. Conf. Computer Assurance (COMPASS'97),Gaithersburg, Md., June 1997.
[36] C. Heitmeyer, J. Kirby, Jr., B. Labaw, and R. Bharadwaj, "SCR*: A Toolset for Specifying and Analyzing Software Requirements," Proc. Computer-Aided Verification, 10th Ann. Conf. (CAV'98),Vancouver, Canada, 1998.
[37] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, "Tools for Analyzing SCR-Style Requirements Specifications: A Formal Foundation," technical report, Naval Research Laboratory, Washington, D.C., 1998. Draft.
[38] K. Heninger, D.L. Parnas, J.E. Shore, and J.W. Kallander, "Software Requirements for the A-7E Aircraft," Technical Report 3876, Naval Research Laboratory, Washington, D.C., 1978.
[39] K.L. Heninger, "Specifying Software Requirements for Complex Systems: New Techniques and Their Application," IEEE Trans. Software Eng., vol. 6, no. 1, pp. 2-13, Jan. 1980.
[40] S.D. Hester, D.L. Parnas, and D.F. Utter, "Using Documentation as a Software Design Medium," Bell System Technical J., vol. 60, no. 8, pp. 1941-1977, Oct. 1981.
[41] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[42] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[43] D. Jackson, "Requirements and Model Checking," minitutorial, Third Int'l IEEE Symp. Requirements Eng., Jan. 1997.
[44] D. Jackson, S. Jha, and C.A. Damon, "Faster Checking of Software Specifications Using Isomorphs," Proc., Principles of Programming Languages (POPL), 1994.
[45] F. Jahanian and A.K. Mok, "Modechart: A Specification Language for Real-Time Systems," IEEE Trans. Software Eng., vol. 20, no. 10, pp. 879-889, Oct. 1994.
[46] R. Jeffords and C. Heitmeyer, "Automatic Generation of State Invariants from Requirements Specifications," Proc. Sixth ACM SIGSOFT Symp. Foundations of Software Eng., Nov. 1998.
[47] J. Kirby, Jr., "Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System," Technical Report TR-87-07, Wang Inst. of Graduate Studies, 1987.
[48] R.P. Kurshan, "Formal Verification in a Commercial Setting. Proc. Design Automation Conf., June 1997.
[49] R.P. Kurshan, "Reducibility in Analysis of Coordination," P. Varaiya and A.B. Kurzhanski, eds., Discrete Event Systems: Models and Applications, pp. 19-39.New York: Springer-Verlag, 1987.
[50] R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton Univ. Press, 1994.
[51] C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem, "Property Preserving Abstractions for the Verification of Concurrent Systems," Formal Methods in System Design, vol. 6, pp. 1-35, 1995.
[52] R. Lutz, "Targeting Safety-Related Errors During Software Requirements Analysis," Proc. First ACM SIGSOFT Symp.The Foundations of Software Engineering, 1993.
[53] R.R. Lutz and H.-Y. Shaw, "Applying the SCR* Requirements Toolset to DS-1 Fault Protection," Technical Report JPL-D15198, Jet Propulsion Laboratory, Pasadena, Calif., Dec. 1997.
[54] D. Mandrioli, A. Morzenti, M. Pezze, P. SanPietro, and S. Silva, "A Petri Net and Logic Approach to the Specification and Analysis of Real-Time Systems," C. Heitmeyer and Dino Mandrioli, eds., Formal Methods for Real-Time Computing, Trends in Software.Chichester, England: John Wiley&Sons Ltd, 1996.
[55] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[56] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[57] S. Meyer and S. White, "Software Requirements Methodology and Tool Study for A6-E Technology Transfer," technical report, Grumman Aerospace Corp., Bethpage, New York, July 1983.
[58] S. Miller, "Specifying the Mode Logic of a Flight Guidance Ssystem in CoRE and SCR," Proc. Second ACM Workshop Formal Methods in Software Practice (FMSP'98), 1998.
[59] J. Ostroff, "A Visual Toolset for the Design of Real-Time Discrete-Event Systems," IEEE Trans. Control Systems Technology, vol. 5, no. 3, pp. 320-337, May 1997.
[60] D.L. Parnas, G.J.K. Asmis, and J. Madey, "Assessment of Safety-Critical Software in Nuclear Power Plants," Nuclear Safety, vol. 32, no. 2, pp. 189-198, Apr.-June 1991.
[61] D.L. Parnas and J. Madey, “Functional Documentation for Computer Systems,” Science of Computer Programming, vol. 25, no. 1, pp. 41–61, Oct. 1995.
[62] T. Sreemani and J.M. Atlee, "Feasibility of Model Checking Software Requirements," Proc. 11th Ann. Conf. Computer Assurance (COMPASS'96),Gaithersburg, Md., June 1996.
[63] J. Sutton personal communication, Sept. 1997.
[64] U.S. General Accounting Office, "Mission Critical Systems: Defense Attempting to Address Major Software Challenges," Technical Report GAO/IMTEC-93-13, U.S. General Accounting Office, Washington, D.C., Dec. 1992.
[65] M. Weiser, "Program Slicing," IEEE Trans. Software Eng., vol. 10, no. 4, pp. 352-357, July 1984.
[66] M. Young, "How to Leave out Details: Error Preserving Abstractions of State-Space Models," Proc. ACM Conf. Software Testing, Analysis and Verification, 1988.

Index Terms:
Requirements, specification, abstraction, model checking, formal methods, verification, safety analysis, simulation, consistency checking, SCR.
Citation:
Constance Heitmeyer, James Kirby, Jr., Bruce Labaw, Myla Archer, Ramesh Bharadwaj, "Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications," IEEE Transactions on Software Engineering, vol. 24, no. 11, pp. 927-948, Nov. 1998, doi:10.1109/32.730543
Usage of this product signifies your acceptance of the Terms of Use.