Model-based test case generation using symbolic execution

ABSTRACT

In this paper, we present a test case generation method in which test cases are generated from Excel-based functional specications, called error-check/update specications. This method has the following two characteristics. 1) Logical structures and constraint conditions in error-check/update specications are translated into Java code. Then the trans- lated Java code is executed symbolically. A solution found by solving combinations of the constraint conditions, during the symbolic execution can serve as a test case for the Excel- based specication. 2)We present test case selection method to extract a suitable test-suite from the large number of test cases typically generated by the above symbolic execution. Our test case selection is based on a path condition-based test case selection criterion, proposed in our previous work, in which the selected test cases covers all the atomic conditions of path conditions collected during symbolic execution. In this paper, we extend this method with classication of test cases and priority of variable values with the aim of improv- ing the quality of the selected test-suite. We implemented the test case generation method in our tool and evaluated this method with Excel-based test specications for a real- world nancial system.

References

1. S. Anand, C. S. Păsăreanu, and W. Visser. Jpf-se: a symbolic execution extension to java pathfinder. In TACAS’07, TACAS’07, pages 134–138, Berlin, Heidelberg, 2007. Springer-Verlag.
2. B. Beizer. Software testing techniques (2nd ed.). Van Nostrand Reinhold Co., New York, NY, USA, 1990.
3. C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209–224, 2008.
4. P. Godefroid, N. Klarlund, and K. Sen. Dart: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, PLDI ’05, pages 213–223, New York, NY, USA, 2005. ACM.
5. J. C. King. Symbolic execution and program testing. Commun. ACM, 19:385–394, July 1976.
6. K. Munakata, S. Fujiwara, S. Tokumoto, and T. Uehara. Test case selection based on path conditions of symbolic execution. In K. R. P. H. Leung and P. Muenchaisri, editors, APSEC, pages 318–321. IEEE, 2012.
7. C. S. Pˇasˇareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In Proceedings of the 2008 international symposium on Software testing and analysis, ISSTA ’08, pages 15–26, New York, NY, USA, 2008. ACM.
8. M. Utting, A. Pretschner, and B. Legeard. A taxonomy of model-based testing, 2006.

Index Terms

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging