
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 498520, July, 1998.  
BibTex  x  
@article{ 10.1109/32.708566, author = {William Chan and Richard J. Anderson and Paul Beame and Steve Burns and Francesmary Modugno and David Notkin and Jon D. Reese}, title = {Model Checking Large Software Specifications}, journal ={IEEE Transactions on Software Engineering}, volume = {24}, number = {7}, issn = {00985589}, year = {1998}, pages = {498520}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.708566}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Model Checking Large Software Specifications IS  7 SN  00985589 SP498 EP520 EPD  498520 A1  William Chan, A1  Richard J. Anderson, A1  Paul Beame, A1  Steve Burns, A1  Francesmary Modugno, A1  David Notkin, A1  Jon D. Reese, PY  1998 KW  Formal methods KW  statebased specifications KW  requirements KW  statecharts KW  symbolic model checking KW  binary decision diagrams KW  software verification. VL  24 JA  IEEE Transactions on Software Engineering ER   
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 statebased 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 A7E Aircraft," technical report, Naval Research Laboratory, Mar. 1988.
[2] R. Alur, C. Courcoubetis, and D. Dill, “ModelChecking for RealTime 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. 334, 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.: SpringerVerlag, 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. 87152, 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. 533535.
[9] B. Boigelot and P. Godefroid, "Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs," Alur and Henzinger [4], pp. 112.
[10] R.E. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[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. 206213, Feb. 1991.
[12] R.E. Bryant and Y.A. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Technical Report CMUCS94160, 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. 535541, 1995.
[14] M. Vidyasagar, “Statistical Learning Theory and Randomized Algorithms for Control,” IEEE Control Systems, pp. 6985, 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. ComputerAided Design of Integrated Circuits, vol. 13, no. 4, pp. 401424, 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. 142170, 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 NonLinear Constraints," Grumberg [30], pp. 316327.
[18] W. Chan, R.J. Anderson, P. Beame, and D. Notkin, "Improving Efficiency of Symbolic Model Checking for StateBased System Requirements," M. Young, ed., ISSTA'98: Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 102112,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 finitestate concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 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. 645648,Las Vegas, ACM/IEEE, June 1996.
[22] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A SemanticsBased Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 3672.
[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. 4048, 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. 131149. SpringerVerlag, 1995.
[26] D.L. Dill, "The${\rm Mur}\varphi$Verification System," Alur and Henzinger [4], pp. 390393.
[27] M.B. Dwyer, G.S. Avrunin, and J.C. Corbet, "Property Specification Patterns for FiniteState Verification," M. Ardis, ed., Proc. FMSP'98: The Second Workshop Formal Methods in Software Practice, pp. 715,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. 1726.
[30] Computer Aided Verification, Proc. Ninth Int'l Conf., CAV'97, Lecture Notes in Computer Science 1,254, O. Grumberg, ed., Haifa, Israel. SpringerVerlag, 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. 293333, Oct. 1996.
[33] M.P.E. Heimdahl and B.J. Czerny, "Using PVS to Analyze Hierarchical StateBased 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 StateBased Requirements," IEEE Trans. Software Eng., pp. 363377, vol. 22, June 1996.
[35] J. Helbig and P. Kelb, "An OBDDRepresentation 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. 142149,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. 212, 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. 453462,Milwaukee, Wisconsin, IEEE, Oct. 1995.
[38] T.A. Henzinger, P.H. Ho, and H. WongToi, "HyTech: A Model Checker for Hybrid Systems," Grumberg [30], pp. 460463.
[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. 519531,Barcelona, Spain. SpringerVerlag, 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. 48495, July 1996.
[41] M.S. Jaffe, N.G. Leveson, M.P.E. Heimdahl, and B. Melhart, "Software Requirements Analysis for RealTime ProcessControl Systems," IEEE Trans. Software Engineering, vol. 17, no. 3, pp. 241258, 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. AddisonWesley, 1995.
[44] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for ProcessControl Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684707, 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. 314319,San Diego, June 1994.
[47] R. Milner, "An Algebraic Definition of Simulation Between Programs," Proc. Second Int'l Joint Conf. Artificial Intelligence, pp. 481489, 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. 411414.
[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. 245264. SpringerVerlag, 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. 425444,Oxford, U.K.: SpringerVerlag, 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 ComputerAided Design: First Int'l Conf., FMCAD'96 Proc., pp. 389403,Palo Alto, Calif., SpringerVerlag, 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. 232243,Vancouver, Canada, SpringerVerlag, June/July 1998.
[55] J.M. Wing and M. VaziriFarahani, "A Case Study in Model Checking Software Systems," Science of Computer Programming, vol. 28, nos. 2/3, pp. 273299, Apr. 1997.
[56] J. Yang, A.K. Mok, and F. Wang, "Symbolic Model Checking for EventDriven RealTime Systems," ACM Trans. Programming Languages and Systems, vol. 19, no. 2, pp. 386412, Mar. 1997.