|
 ABSTRACT
This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.To generate test cases for a method, Korat constructs a Java predicate (i.e., a method that returns a boolean) from the method's pre-condition. The heart of Korat is a technique for automatic test case generation: given a predicate and a bound on the size of its inputs, Korat generates all (nonisomorphic) inputs for which the predicate returns true. Korat exhaustively explores the bounded input space of the predicate but does so efficiently by monitoring the predicate's executions and pruning large portions of the search space.This paper illustrates the use of Korat for testing several data structures, including some from the Java Collections Framework. The experimental results show that it is feasible to generate test cases from Java predicates, even when the search space for inputs is very large. This paper also compares Korat with a testing framework based on declarative specifications. Contrary to our initial expectation, the experiments show that Korat generates test cases much faster than the declarative framework.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
William Adjie-Winoto , Elliot Schwartz , Hari Balakrishnan , Jeremy Lilley, The design and implementation of an intentional naming system, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.186-201, December 12-15, 1999, Charleston, South Carolina, United States
|
| |
2
|
T. Ball, D. Hoffman, F. Ruskey, R. Webber, and L. J. White. State generation and automated class testing. Software Testing, Verification & Reliability, 10(3):149-170, 2000.
|
| |
3
|
K. Bech and E. Gamma. Test infected: Programmers love writing tests. Java Report, 3(7), July 1998.
|
| |
4
|
|
| |
5
|
|
| |
6
|
Y. Cheon and G. T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. Technical Report 01-12, Department of Computer Science, Iowa State University, Nov. 2001.
|
| |
7
|
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]
|
| |
8
|
|
| |
9
|
|
| |
10
|
D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998.
|
| |
11
|
|
| |
12
|
|
| |
13
|
|
| |
14
|
|
| |
15
|
|
| |
16
|
|
| |
17
|
|
| |
18
|
|
| |
19
|
|
| |
20
|
G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, June 1998. (last revision: Aug 2001).
|
| |
21
|
|
| |
22
|
|
| |
23
|
|
| |
24
|
|
| |
25
|
J. Offutt and A. Abdurazik. Generating tests from UML specifications. In Proc. Second International Conference on the Unified Modeling Language, Oct. 1999.
|
| |
26
|
|
| |
27
|
|
| |
28
|
|
| |
29
|
I. Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.
|
| |
30
|
N. J. A. Sloane, S. Plouffe, J. M. Borwein, and R. M. Corless. The encyclopedia of integer sequences. SIAM Review, 38(2), 1996. http://www.research.att.com/~njas/sequences/Seis.html.
|
| |
31
|
|
| |
32
|
|
CITED BY 73
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Vinod Ganapathy , Sanjit A. Seshia , Somesh Jha , Thomas W. Reps , Randal E. Bryant, Automatic discovery of API-level exploits, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Cyrille Artho , Howard Barringer , Allen Goldberg , Klaus Havelund , Sarfraz Khurshid , Mike Lowry , Corina Pasareanu , Grigore Rosu , Koushik Sen , Willem Visser , Rich Washington, Combining test case generation and runtime verification, Theoretical Computer Science, v.336 n.2-3, p.209-234, 26 May 2005
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Brian Demsky , Michael D. Ernst , Philip J. Guo , Stephen McCamant , Jeff H. Perkins , Martin Rinard, Inference and enforcement of data structure consistency specifications, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Marc Fisher, II , Gregg Rothermel , Darren Brown , Mingming Cao , Curtis Cook , Margaret Burnett, Integrating automated test generation into the WYSIWYT spreadsheet testing methodology, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.2, p.150-194, April 2006
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sebastian Elbaum , Hui Nee Chin , Matthew B. Dwyer , Jonathan Dokulil, Carving differential unit test cases from system test cases, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
|
|
|
|
|
|
Andreas Leitner , Ilinca Ciupa , Manuel Oriol , Bertrand Meyer , Arno Fiva, Contract driven development = test driven development - writing test cases, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
|
|
|
|
|
|
Sriram Sankaranarayanan , Swarat Chaudhuri , Franjo Ivančić , Aarti Gupta, Dynamic inference of likely data preconditions over predicates by tree learning, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sasa Misailovic , Aleksandar Milicevic , Nemanja Petrovic , Sarfraz Khurshid , Darko Marinov, Parallel test generation and execution with Korat, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bassem Elkarablieh , Ivan Garcia , Yuk Lai Suen , Sarfraz Khurshid, Assertion-based repair of complex data structures, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf