This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Model Checking Large Software Specifications
July 1998 (vol. 24 no. 7)
pp. 498-520

Abstract—In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems.

[1] T. Alspaugh, S. Faulk, K. Britton, R. Parker, D. Parnas, and J. Shore, "Software Requirements for the A-7E Aircraft," technical report, Naval Research Laboratory, Mar. 1988.
[2] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[3] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[4] R. Alur and T.A. Henzinger, eds. Computer Aided Verification. Proc. Eighth Int'l Conf., CAV'96, Lecture Notes in Computer Science 1102.New Brunswick, N.J.: Springer-Verlag, July/Aug. 1996.
[5] 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.
[6] G. Berry and G. Gonthier, "The ESTERELSynchronous Programming Language: Design, Semantics, Implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[7] R. Bharadwaj and C. Heitmeyer, "Verifying SCR Requirements Specifications Using State Exploration," Proc. First ACM SIGPLAN Workshop Automatic Analysis of Software,Paris, France, Jan. 1997.
[8] B. Boehm, Software Engineering Economics, Prentice Hall, Upper Saddle River, N.J., 1981, pp. 533-535.
[9] B. Boigelot and P. Godefroid, "Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs," Alur and Henzinger [4], pp. 1-12.
[10] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[11] R.E. Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication," IEEE Trans. Computers, vol. 40, no. 2, pp. 206-213, Feb. 1991.
[12] R.E. Bryant and Y.-A. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Technical Report CMU-CS-94-160, School of Computer Science, Carnegie Mellon Univ., June 1994.
[13] R.E. Bryant and Y. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Proc. 32nd Design Automation Conf., pp. 535-541, 1995.
[14] M. Vidyasagar, “Statistical Learning Theory and Randomized Algorithms for Control,” IEEE Control Systems, pp. 69-85, Dec. 1998.
[15] J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Trans. Computer-Aided Design of Integrated Circuits, vol. 13, no. 4, pp. 401-424, Apr. 1994.
[16] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang., "Symbolic model checking: 1020states and beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[17] W. Chan, R.J. Anderson, P. Beame, and D. Notkin, "Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-Linear Constraints," Grumberg [30], pp. 316-327.
[18] W. Chan, R.J. Anderson, P. Beame, and D. Notkin, "Improving Efficiency of Symbolic Model Checking for State-Based System Requirements," M. Young, ed., ISSTA'98: Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 102-112,Clearwater Beach, Fla., Mar. 1998. Also published as Software Engineering Notes, vol. 23, no. 2, Mar. 1998.
[19] 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.
[20] E.M. Clarke, R. Enders, T. Filkorn, and S. Jha, “Exploiting Symmetries in Temporal Model Logic Model Checking,” Formal Methods in System Design, vol. 9, 1996.
[21] E.M. Clarke, M. Khaira, and X. Zhao, "Word Level Model Checking—Avoiding the Pentium FDIV Error," Proc. 33rd Design Automation Conf., pp. 645-648,Las Vegas, ACM/IEEE, June 1996.
[22] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[23] J.C. Corbett, “Evaluating Deadlock Detection Methods for Concurrent Software,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161–179, Mar. 1996.
[24] J. Crow and B.L. Di Vito, "Formalizing Space Shuttle Software Requirements," Proc. ACM SIGSOFT Workshop Formal Methods in Software Practice, pp. 40-48, Jan. 1996.
[25] W. Damm, H. Hungar, P. Kelb, and R. Schlör, "Statecharts: Using Graphical Specification Languages and Symbolic Model Checking in the Verification of a Production Cell," C. Lewerentz and T. Lindner, eds., Formal Development of Reactive Systems: Case Study Production Cell, Lecture Notes in Computer Science 891, pp. 131-149. Springer-Verlag, 1995.
[26] D.L. Dill, "The${\rm Mur}\varphi$Verification System," Alur and Henzinger [4], pp. 390-393.
[27] M.B. Dwyer, G.S. Avrunin, and J.C. Corbet, "Property Specification Patterns for Finite-State Verification," M. Ardis, ed., Proc. FMSP'98: The Second Workshop Formal Methods in Software Practice, pp. 7-15,Clearwater Beach, Fla., Mar. 1998.
[28] Federal Aviation Administration, U.S. Dept. of Transportation, Introduction to TCAS II, Mar. 1990.
[29] D. Garlan et al., "Architectural Mismatch: Why Reuse is So Hard", IEEE Software, Nov. 1995, pp. 17-26.
[30] Computer Aided Verification, Proc. Ninth Int'l Conf., CAV'97, Lecture Notes in Computer Science 1,254, O. Grumberg, ed., Haifa, Israel. Springer-Verlag, June 1997.
[31] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[32] D. Harel and A. Naamad, "The STATEMATE Semantics of Statecharts," ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 293-333, Oct. 1996.
[33] M.P.E. Heimdahl and B.J. Czerny, "Using PVS to Analyze Hierarchical State-Based Requirements for Completeness and Consistency," Proc. IEEE High Assurance Systems Eng. Workshop,Niagara Falls, Canada, Oct. 1996.
[34] 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.
[35] J. Helbig and P. Kelb, "An OBDD-Representation of Statecharts," Proc.: The European Design and Test Conf. EDAC, The European Conf. Design Automation. ETC, European Test Conf. EUROASIC, The European Event in ASIC Design, pp. 142-149,Paris, France, IEEE, Feb./Mar. 1994.
[36] K. Heninger, "Specifying Software Requirements for Complex Systems: New Techniques and Their Applications," IEEE Trans. Software Eng., vol. 6, no. 1, pp. 2-12, Jan. 1980.
[37] M.R. Henzinger, T.A. Henzinger, and P.W. Kopke, "Computing Simulations on Finite and Infinite Graphs," Proc.: 36th Ann. Symp. Foundations of Computer Science, pp. 453-462,Milwaukee, Wisconsin, IEEE, Oct. 1995.
[38] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: A Model Checker for Hybrid Systems," Grumberg [30], pp. 460-463.
[39] D. Jackson, "Abstract Model Checking of Infinite Specifications," M. Naftalin, T. Denvir, and M. Bertran, eds., FME'94: Industrial Benefit of Formal Methods, Proc. Second Int'l Symp. Formal Methods Europe, Lecture Notes in Computer Science 873, pp. 519-531,Barcelona, Spain. Springer-Verlag, Oct. 1994.
[40] D. Jackson and C.A. Damon, "Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector," IEEE Trans. Software Eng., vol. 22, no. 7, pp. 484-95, July 1996.
[41] M.S. Jaffe, N.G. Leveson, M.P.E. Heimdahl, and B. Melhart, "Software Requirements Analysis for Real-Time Process-Control Systems," IEEE Trans. Software Engineering, vol. 17, no. 3, pp. 241-258, Mar. 1991.
[42] M.Y. Vardi and O. Kupferman, “Module Checking,” Proc. Conf. Computer Aided Verification (CAV '96), 1996.
[43] N.G. Leveson, Safeware: System Safety and Computers. Addison-Wesley, 1995.
[44] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[45] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[46] K.L. McMillan, "Fitting Formal Methods into the Design Cycle," Proc. 31st ACM/IEEE Design Automation Conf., pp. 314-319,San Diego, June 1994.
[47] R. Milner, "An Algebraic Definition of Simulation Between Programs," Proc. Second Int'l Joint Conf. Artificial Intelligence, pp. 481-489, Sept. 1971.
[48] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas, "PVS: Combining Specification, Proof Checking, and Model Checking," Alur and Henzinger [4], pp. 411-414.
[49] A. Pnueli and M. Shalev, "What is in a Step: On the Semantics of Statecharts," Proc. Int'l Conf. Theoretical Aspects of Computer Software, pp. 245-264. Springer-Verlag, Sept. 1991.
[50] R. Pugliese and E. Tronci, "Automatic Verification of a Hydro- electric Power Plant," M.-C. Gaudel and J. Woodcock, eds., FME'96: Industrial Benefit and Advances in Formal Methods, Proc. Third Int'l Symp. Formal Methods Europe, Lecture Notes in Computer Science 1051, pp. 425-444,Oxford, U.K.: Springer-Verlag, Mar. 1996.
[51] J.D. Reese and N. Leveson, “Software Deviation Analysis,” Proc. 19th Int'l Conf. Software Eng. (ICSE '97), pp. 250–260, May 1997.
[52] E.M. Sentovich, "A Brief Study of BDD Package Performance," M. Srivas and A. Camilleri, eds., Formal Methods in Computer-Aided Design: First Int'l Conf., FMCAD'96 Proc., pp. 389-403,Palo Alto, Calif., Springer-Verlag, Nov. 1996..
[53] T. Sreemani and J.M. Atlee, "Feasibility of Model Checking Software Requirements," Proc. 11th Ann. Conf. Computer Assurance (COMPASS'96),Gaithersburg, Md., June 1996.
[54] J.S. Thathachar, "On the Limitations of Ordered Representations of Functions," A. Hu and M. Vardi, eds., Proc. Computer Aided Verification, 10th Int'l Conf., CAV'98, Lecture Notes in Computer Science, pp. 232-243,Vancouver, Canada, Springer-Verlag, June/July 1998.
[55] J.M. Wing and M. Vaziri-Farahani, "A Case Study in Model Checking Software Systems," Science of Computer Programming, vol. 28, nos. 2/3, pp. 273-299, Apr. 1997.
[56] J. Yang, A.K. Mok, and F. Wang, "Symbolic Model Checking for Event-Driven Real-Time Systems," ACM Trans. Programming Languages and Systems, vol. 19, no. 2, pp. 386-412, Mar. 1997.

Index Terms:
Formal methods, state-based specifications, requirements, statecharts, symbolic model checking, binary decision diagrams, software verification.
Citation:
William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, Jon D. Reese, "Model Checking Large Software Specifications," IEEE Transactions on Software Engineering, vol. 24, no. 7, pp. 498-520, July 1998, doi:10.1109/32.708566
Usage of this product signifies your acceptance of the Terms of Use.