Korat: Automated testing based on Java predicates

Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
EditorsP.G. Frankl, P.G. Frankl
Pages123-133
Number of pages11
StatePublished - Dec 1 2002
Externally publishedYes
EventISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis - Roma, Italy
Duration: Jul 22 2002Jul 24 2002

Publication series

NameProceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis

Other

OtherISSTA 02 Proceedings of the ACM SIGSOFT 2002 International Symposium on Software Testing and Analysis
CountryItaly
CityRoma
Period7/22/027/24/02

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Korat: Automated testing based on Java predicates'. Together they form a unique fingerprint.

Cite this