Projected state machine coverage for software testing

ABSTRACT

Our research deals with test generation for software based on finite state machine (FSM) models of the program specification. We describe a set of coverage criteria and testing constraints for use in the automatic generation of test suites. We also describe the algorithms used to generate test suites based on these coverage criteria, and the implementation of these algorithms as an extension of the Murϕ model checker[4]. The coverage criteria are simple but powerful in that they generate test suites of high quality and moderate volume, without requiring the user to have a sophisticated grasp of the test generation technology. The testing constraints are used to combat the endemic problem of state explosion, typically encountered in FSM techniques. We illustrate our techniques on several well-known problems from the literature and describe two industrial trials, to demonstrate the validity of our claims.

REFERENCES

• 1: Richard H. Carver , Kuo-Chung Tai, Use of Sequencing Constraints for Specification-Based Testing of Concurrent Programs, IEEE Transactions on Software Engineering, v.24 n.6, p.471-490, June 1998 [doi>10.1109/32.689403]
• 2: Hartman, A., and Nagin, K. M., GOTCHA-TCBeans Tool Overview, Release 3.0.2, 2001 http://www.haifa.il.ibm.com/projects/verification/gtcb/documentation.html.
• 3: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 4: Dill, D., Murϕ Description Language and Verifier, http://sprout.stanford.edu/dill/murphi.html.
• 5: Mullerburg, M.,, Holenderski, L., Maffeis, O., Merceron, A., and Morley, M., Systematic testing and formal verification to validate reactive programs. Software Quality Journal, 4 (1995).
• 6: Helmbold D., and Luckham D., Debugging Ada tasking programs, IEEE Software 2 (1985) 47-57.
• 7: Robin, I. And Turner K. Protocol simulators, http://www.cs.stir.ac.uk/~kjt/software/comms/jasper.
• 8: Farchi, E., Hartman, A., and Pinter, S. S. Using a model-based test generator to test for standards conformance. IBM Systems Journal 41 (2002) 89-110.
• 9: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 10: Gregor V. Bochmann , Alexandre Petrenko, Protocol testing: review of methods and relevance for software testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.109-124, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187153]
• 11: Pramod V. Koppol , Kuo-Chung Tai, An incremental approach to structural testing of concurrent software, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.14-23, January 08-10, 1996, San Diego, California, United States
• 12: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 13: Jean Hartmann , Claudio Imoberdorf , Michael Meisinger, UML-Based integration testing, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.60-70, August 21-24, 2000, Portland, Oregon, United States
• 14: Offut, J., and Abdurazik, A., Generating tests from UML specifications. International Conference on the Unified Modeling Language (1999).
• 15: Thierry Jéron , Pierre Morel, Test Generation Derived from Model-Checking, Proceedings of the 11th International Conference on Computer Aided Verification, p.108-121, July 06-10, 1999
• 16: Henniger, O., and Ural, H., Test generation based on control and data dependencies within multi-process SDL specifications. Proceedings of the 2nd Workshop of the SDL Forum Society on SDL and MSC (2000).
• 17: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Verification

Keywords:
automated test generation, finite state machine modeling, state machine projection., validation