Software model checking in practice: an industrial case study

ABSTRACT

We present an application of software model checking to the analysis of a large industrial software product: Lucent Technologies' CDMA call-processing library. This software is deployed on thousands of base stations in wireless networks world-wide, where it sets up and manages millions of calls to and from mobile devices everyday. Our analysis of this software was carried out using VeriSoft, a tool developed at Bell Laboratories that implements model-checking algorithms for systematically testing concurrent reactive software.VeriSoft has now been used for over a year for analyzing several releases and versions of the CDMA call-processing software. Although we started this work with a fairly robust version of the software, the application of model checking exposed several problems that had escaped traditional testing. Model checking also helped developers maintain a high degree of confidence in the library as it evolved through its many releases and versions.To our knowledge, software model checking has rarely been applied to software systems of this scale. In this paper, we describe our experience in applying this technology in an industrial environment.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 2: Gérard Berry , Georges Gonthier, The ESTEREL synchronous programming language: design, semantics, implementation, Science of Computer Programming, v.19 n.2, p.87-152, Nov. 1992 [doi>10.1016/0167-6423(92)90005-V]
• 3: Bernard Boigelot , Patrice Godefroid, Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.465-478, March 18-22, 1996
• 4: Juei Chang , Debra J. Richardson , Sriram Sankar, Structural specification-based testing with ADL, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.62-70, January 08-10, 1996, San Diego, California, United States
• 5: Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• 8: Christopher Colby, Analyzing the communication topology of concurrent programs, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.202-213, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215592]
• 9: James C. Corbett, Constructing abstract models of concurrent real-time software, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.250-260, January 08-10, 1996, San Diego, California, United States
• 10: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 11: Régis Cridlig, Semantic analysis of shared-memory concurrent languages using abstract model-checking, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.214-225, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215593]
• 12: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 13: Laura K. Dillon , Qing Yu, Oracles for checking temporal properties of concurrent systems, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.140-153, Dec. 1994
• 14: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 15: Jean-Claude Fernandez , Hubert Garavel , Laurent Mounier , Anne Rasse , Carlos Rodriguez , Joseph Sifakis, A toolbox for the verification of LOTOS programs, Proceedings of the 14th international conference on Software engineering, p.246-259, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143124]
• 16: Jean-Claude Fernandez , Claude Jard , Thierry Jéron , César Viho, Using On-The-Fly Verification Techniques for the Generation of test Suites, Proceedings of the 8th International Conference on Computer Aided Verification, p.348-359, August 03, 1996
• 17: A. R. Flora-Holmquist , M. G. Staskauskas, Formal validation of virtual finite state machines, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.122, April 05-08, 1995
• 18: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 19: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 20: Patrice Godefroid , Robert S. Hanmer , Lalita Jategaonkar Jagadeesan, Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.124-133, March 02-04, 1998, Clearwater Beach, Florida, United States
• 21: Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 1990.
• 22: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 23: Gerard J. Holzmann , Joanna Patti, Validating SDL Specifications: an Experiment, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.317-326, June 06-09, 1989
• 24: Gerard J. Holzmann , Margaret H. Smith, A practical method for verifying event-driven software, Proceedings of the 21st international conference on Software engineering, p.597-607, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302710]
• 25: Lalita Jategaonkar Jagadeesan , Adam Porter , Carlos Puchol , J. Christopher Ramming , Lawrence G. Votta, Specification-based testing of reactive software: tools and experiments: experience report, Proceedings of the 19th international conference on Software engineering, p.525-535, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253435]
• 26: Douglas Long , Lori A. Clarke, Data flow analysis of concurrent systems that use the rendezvous model of synchronization, Proceedings of the symposium on Testing, analysis, and verification, p.21-35, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120810]
• 27: Stephen P. Masticola , Barbara G. Ryder, Non-concurrency analysis, Proceedings of the fourth ACM SIGPLAN symposium on Principles and practice of parallel programming, p.129-138, May 19-22, 1993, San Diego, California, United States
• 28: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 29: Debra J. Richardson, TAOS: Testing with Analysis and Oracle Support, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.138-153, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187158]
• 30: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• 31: Arnaud Venet, Abstract Interpretation of the pi-Calculus, Selected papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, p.51-75, June 24-26, 1996
• 32: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 33: Mihalis Yannakakis , David Lee, Testing finite state machines, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.476-485, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103468]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  J. Computer Applications
  J.1 ADMINISTRATIVE DATA PROCESSING
      Subjects: Business

General Terms:
Algorithms, Experimentation, Performance