This Article 
 Bibliographic References 
 Add to: 
An Automated Verification Method for Distributed Systems Software Based on Model Extraction
April 2002 (vol. 28 no. 4)
pp. 364-377

Software verification methods are used only sparingly in industrial software development today. The most successful methods are based on the use of model checking. There are, however, many hurdles to overcome before the use of model checking tools can truly become mainstream. To use a model checker, the user must first define a formal model of the application, and to do so requires specialized knowledge of both the application and of model checking techniques. For larger applications, the effort to manually construct a formal model can take a considerable investment of time and expertise, which can rarely be afforded. Worse, it is hard to secure that a manually constructed model can keep pace with the typical software application, as it evolves from the concept stage to the product stage. In this paper, we describe a verification method that requires far less specialized knowledge in model construction. It allows us to extract models mechanically from source code. The model construction process now becomes easily repeatable, as the application itself continues to evolve. Once the model is constructed, existing model checking techniques allow us to perform all checks in a mechanical fashion, achieving nearly complete automation. The level of thoroughness that can be achieved with this new type of software testing is significantly greater than for conventional techniques. We report on the application of this method in the verification of the call processing software for a new telephone switch that was recently developed at Lucent Technologies.

[1] K. Bartlett, R. Scantlebury, and P. Wilkinson, "A Note on Reliable Full-Duplex Transmission over Half-Duplex Links," Comm. ACM, vol. 12, no. 5, pp. 260-261, May 1969.
[2] Bellcore, LSSGR, LATA Switching Systems Generic Requirements, FR-NWT-000064, 1992 ed. Feature requirements, SPCS Capabilities and Features, Issue 1, Mar. 1996.
[3] Bellcore, LSSGR, LATA Switching Systems Generic Requirements, FR-NWT-000064, 1992 ed. Feature requirements, SPCS Capabilities and Features, FSD 01-02-1450, p. 8, Mar. 1996.
[4] Bellcore, LSSGR, LATA Switching Systems Generic Requirements, FR-NWT-000064, 1992 ed. Feature requirements, SPCS Capabilities and Features, FSD 01-02-1201, p. 2, Mar. 1996.
[5] J.R. Buchi, “On a Decision Method in Restricted Second-Order Arithmetics,” Proc. Int'l Conf. Logic, Methods, and Philosophy of Science, pp. 1-12, 1962.
[6] 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.
[7] J. Chaves, "Formal Methods at AT&T, An Industrial Usage Report," Proc. Fourth FORTE Conf. Formal Description Techniques, pp. 83-90,Sydney, Australia, 1991.
[8] C. Colby, P. Godefroid, and L. Jagadeesan, “Automatically Closing Open Reactive Programs,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 345-357, June 1998.
[9] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng, “Bandera: Extracting Finite-State Models from Java Source Code,” Proc. 22nd Int'l Conf. Software Eng., pp. 439–448, June 2000.
[10] 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.
[11] M.B. Dwyer and C.S. Pasareanu, “Filter-Based Model Checking of Partial Systems,” Proc. ACM SIGSOFT Sixth Int'l Symp. Foundation of Software Eng., Nov. 1998.
[12] R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman&Hall, June 1995.
[13] P. Godefroid, “VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software,” Proc. Nineth Conf. Computer Aided Verification, June 1997.
[14] P. Godefroid, R.S. Hammer, and L. Jagadeesan, “Systematic Software Testing using Verisoft,” Bell Labs Technical J., vol. 3, no. 2, Apr.-June 1998.
[15] J. Hatcliff, M.B. Dwyer, and H. Zheng, “Slicing Software for Model Construction,” J. Higher-Order and Symbolic Computation, vol. 13, no. 4, pp. 315-353, Dec. 2000.
[16] K. Havelund and T. Pressburger, “Model Checking Java Programs Using Java PathFinder,” Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366-381, Apr. 2000.
[17] C.A.R. Hoare,“Communicating sequential processes,” Comm. of the ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.
[18] G.J. Holzmann and J. Patti, “Validating SDL Specifications: An Experiment,” Proc. Conf. Protocol Specification, Testing, and Verification pp. 317-326, June 1989.
[19] G.J. Holzmann, “The Theory and Practice of a Formal Method: NewCoRe,” Proc. IFIP World Computer Congress, vol. I, pp. 35-44, Aug. 1994.
[20] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[21] G.J. Holzmann, “Logic Verification of ANSI-C Code with Spin,” Proc. Seventh Int'l SPIN Workshop Model Checking of Software, Sept. 2000.
[22] B. Marick, The Craft of Software Testing. Englewood Cliffs, N.J.: Prentice Hall, 1995.
[23] L. Millett and T. Teitelbaum, “Slicing Promela and its Applications to Protocol Understanding and Analysis,” Proc. Fourth Spin Workshop, Nov. 1998.
[24] P. Pike, D. Presotto, S. Dorward, B. Flandrena, K. Thompson, H. Trickey, and P. Winterbottom, “Plan 9 from Bell Labs,” Computing Systems, vol. 8, no. 3, pp. 221-254, 1995.
[25] A. Pnueli, “The Temporal Logic of Programs,” Proc. 18th IEEE Symp. Foundations of Computer Science, pp. 46-57, 1977.
[26] R. Saracco, J.R.W. Smith, and R. Reed, Telecommunications Systems Engineering using SDL. p. 632, North-Holland, 1989.
[27] S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson, “Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs,” ACM Trans. Computer Systems vol. 15, no. 4, pp. 391-411, Nov. 1997.
[28] F. Tip, “A Survey of Program Slicing Techniques,” J. Programming Languages vol. 3, no. 3, pp. 121-189, Sept. 1995.
[29] W. Visser, S. Park, and J. Penix, “Applying Predicate Abstraction to Model Checking Object-Oriented Programs,” Proc. Third ACM SOGSOFT Workshop Formal Methods in Software Practice, Aug. 2000.

Index Terms:
formal methods, model checking, software verification, software testing, reactive systems, call processing, feature interaction, case studies
G.J. Holzmann, M.H. Smith, "An Automated Verification Method for Distributed Systems Software Based on Model Extraction," IEEE Transactions on Software Engineering, vol. 28, no. 4, pp. 364-377, April 2002, doi:10.1109/TSE.2002.995426
Usage of this product signifies your acceptance of the Terms of Use.