Test Case Generation using Java Path Finder and Symbolic Path Finder

Abstract

Test suite plays an important role in software testing. Good test cases may improve the quality of software by detecting failures earlier. Automation test case generation can help to generate good test cases is needed. Symbolic Path Finder (SPF) is a model checker developed by the National Aeronautics and Space Administration (NASA) as an extension of Java Path Finder (JPF). SPF uses symbolic execution, model checking and constraint solver to produce test cases. This study is intended to perform SPF and to verify the effectiveness of the test case produced by the SPF. Mutation testing, a fault-based testing technique, is conducted to investigate the adequacy of produced test cases. The programs under test in this study are Median, Armstrong, Multiple, Nested If, and Simple Calculator. All those programs are written in the Java programming language. The test suite for each of the programs under test has been generated by applying SPF. The mutation score obtained for produced test suites of each program ae as follows: 74.82% for the Median Program, 77.78% for the Armstrong Program, 31.20% for the Multiple Program, 92.00% for the Nested If Program, and 55.82% for the Simple Calculator Program. These experimental results indicate that the test suite generated by the SPF is unable to detect all existing faults. From the observations, this problem is because SPF only applies decision coverage in determining path during the process of forming test cases. Potential improvement may be obtained by applying other types of coverage criteria.