AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
Korat executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output

Korat: automated testing based on Java predicates

ISSTA, no. 4 (2002): 123-133

Cited by: 778|Views124
EI

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 ...More

Code:

Data:

0
Introduction
  • In general, and test data generation, in particular, are labor-intensive processes.
  • This paper presents Korat, a novel framework for automated testing of Java programs.
  • Korat uses specification-based testing [5, 13, 15, 25].
  • 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 executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output
Highlights
  • Manual software testing, in general, and test data generation, in particular, are labor-intensive processes
  • Korat executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output
  • The previous section focused on automatic test case generation from a Java predicate and a finitization description
  • Korat uses a large subset of Java Modeling Language (JML) that can be automatically translated into Java predicates
  • The heart of Korat is a technique for automatic test case generation: given a predicate and a finitization for its inputs, Korat generates all nonisomorphic inputs for which the predicate returns true
Methods
  • The previous section focused on automatic test case generation from a Java predicate and a finitization description.
  • The authors present how Korat builds on this technique to check correctness of methods.
  • Korat uses specification-based testing: to test a method, Korat first generates test inputs from the method’s precondition, invokes the method on each of those inputs, and checks the correctness of the output using the method’s postcondition.
  • Korat uses a large subset of JML that can be automatically translated into Java predicates
Results
  • The authors present the performance results of the Korat prototype. The authors used Java to implement the search for valid nonisomorphic repOk inputs.
  • For automatic instrumentation of repOk, the authors modified the sources of the Sun’s javac compiler.
  • The authors slightly modified the JML tool-set, building on the existing JML+JUnit framework [6].
  • The authors first present Korat’s performance for test case generation, compare Korat with the test generation that uses Alloy Analyzer [16], and present Korat’s performance for checking method correctness.
  • The authors performed all experiments on a Linux machine with a Pentium III 800 MHz processor using Sun’s Java 2 SDK1.3.1 JVM
Conclusion
  • This paper presented 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 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 from the method’s precondition.
  • Korat exhaustively explores the input space of the predicate, but does so efficiently by: 1) monitoring the predicate’s executions to prune large portions of the search space and 2) generating only nonisomorphic inputs
Tables
  • Table1: Table 1
  • Table2: Benchmarks and finitization parameters. Each benchmark is named after the class for which data structures are generated; the structures also contain objects from other classes
  • Table3: Korat’s performance on several benchmarks. All finitization parameters are set to the size value. Time is the elapsed real time in seconds for the entire generation. State size is rounded to the nearest smaller exponent of two
  • Table4: Performance comparison. For each benchmark, performances of Korat and AA are compared for a range of finitization values. For values larger than presented, AA does not complete its generation within 1 hour. Korat’s performance for larger values is given in Table 3
  • Table5: Korat’s performance on several methods. All upperlimiting finitization parameters for method inputs are set to the given maximum size. These sizes give complete statement coverage. Times are the elapsed real times in seconds for the entire generation of all valid test cases and testing of methods for all those inputs. These times include writing and reading of files with test cases
Download tables as Excel
Related work
  • 6.1 Specification-based testing

    There is a large body of research on specification-based testing. An early paper by Goodenough and Gerhart [13] emphasizes its importance. Many projects automate test case generation from specifications, such as Z specifications [15, 31], UML statecharts [25, 26], or ADL specifications [5, 28]. These specifications typically do not consider linked data structures, and the tools do not generate Java test cases.

    The TestEra framework [22] generates Java test cases from Alloy [17] specifications of linked data structures. TestEra uses the Alloy Analyzer (AA) [16] to automatically generate method inputs and check correctness of outputs, but it requires programmers to learn a specification language much different than Java. Korat generates inputs directly from Java predicates and uses the Java Modeling Language (JML) [20] for specifications. The experimental results also show that Korat generates test cases faster and for larger scopes than AA.
Funding
  • This work was funded in part by NSF grant CCR00-86154
Reference
  • W. Adjie-Winoto, E. Schwartz, H. Balakrishnan, and J. Lilley. The design and implementation of an intentional naming system. In Proc. 17th ACM Symposium on Operating Systems (SOSP), Kiawah Island, Dec. 1999.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • K. Bech and E. Gamma. Test infected: Programmers love writing tests. Java Report, 3(7), July 1998.
    Google ScholarLocate open access versionFindings
  • B. Beizer. Software Testing Techniques. International Thomson Computer Press, 1990.
    Google ScholarFindings
  • J. Chang and D. J. Richardson. Structural specification-based testing: Automated support and experimental evaluation. In Proc. 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 285–302, Sept. 1999.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd International Conference on Software Engineering (ICSE), June 2000.
    Google ScholarLocate open access versionFindings
  • T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, Cambridge, MA, 1990.
    Google ScholarFindings
  • C. Demartini, R. Iosif, and R. Sisto. A deadlock detection tool for concurrent Java programs. Software - Practice and Experience, July 1999.
    Google ScholarFindings
  • D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998.
    Google ScholarLocate open access versionFindings
  • E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements od Reusable Object-Oriented Software. Addison-Wesley Professional Computing Series. Addison-Wesley Publishing Company, New York, NY, 1995.
    Google ScholarFindings
  • P. Godefroid. Model checking for programming languages using VeriSoft. In Proc. 24th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 174–186, Paris, France, Jan. 1997.
    Google ScholarLocate open access versionFindings
  • J. Goodenough and S. Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering, June 1975.
    Google ScholarLocate open access versionFindings
  • G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), May 1997.
    Google ScholarLocate open access versionFindings
  • H.-M. Horcher. Improving software tests using Z specifications. In Proc. 9th International Conference of Z Users, The Z Formal Specification Notation, 1995.
    Google ScholarLocate open access versionFindings
  • D. Jackson, I. Schechter, and I. Shlyakhter. ALCOA: The Alloy constraint analyzer. In Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland, June 2000.
    Google ScholarLocate open access versionFindings
  • D. Jackson, I. Shlyakhter, and M. Sridharan. A micromodularity mechanism. In Proc. 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Vienna, Austria, Sept. 2001.
    Google ScholarLocate open access versionFindings
  • D. Jackson and M. Vaziri. Finding bugs with a constraint solver. In Proc. International Symposium on Software Testing and Analysis (ISSTA), Portland, OR, Aug. 2000.
    Google ScholarLocate open access versionFindings
  • V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Proc. 29th Annual ACM Symposium on the Principles of Programming Languages (POPL), Portland, OR, Jan. 2002.
    Google ScholarLocate open access versionFindings
  • 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).
    Google ScholarFindings
  • B. Liskov. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000.
    Google ScholarFindings
  • D. Marinov and S. Khurshid. TestEra: A novel framework for automated testing of Java programs. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA, Nov. 2001.
    Google ScholarLocate open access versionFindings
  • K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
    Google ScholarFindings
  • A. Moeller and M. I. Schwartzbach. The pointer assertion logic engine. In Proc. SIGPLAN Conference on Programming Languages Design and Implementation, Snowbird, UT, June 2001.
    Google ScholarLocate open access versionFindings
  • J. Offutt and A. Abdurazik. Generating tests from UML specifications. In Proc. Second International Conference on the Unified Modeling Language, Oct. 1999.
    Google ScholarLocate open access versionFindings
  • J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison-Wesley Object Technology Series, 1998.
    Google ScholarLocate open access versionFindings
  • M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst., January 1998.
    Google ScholarLocate open access versionFindings
  • S. Sankar and R. Hayes. Specifying and testing software components using ADL. Technical Report SMLI TR-94-23, Sun Microsystems Laboratories, Inc., Mountain View, CA, Apr. 1994.
    Google ScholarFindings
  • I. Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.
    Google ScholarLocate open access versionFindings
  • 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.
    Locate open access versionFindings
  • J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992.
    Google ScholarFindings
  • W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proc. 15th IEEE International Conference on Automated Software Engineering (ASE), Grenoble, France, 2000.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科