Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/1512762.1512764acmconferencesArticle/Chapter ViewAbstractPublication PageslcsdConference Proceedingsconference-collections
research-article

Whispec: white-box testing of libraries using declarative specifications

Published: 21 October 2007 Publication History

Abstract

We present a novel framework, Whispec, for white-box testing of methods that manipulate structurally complex data, such as those that pervade library classes. Given method preconditions as declarative constraints, our framework systematically generates test inputs for the methods to maximize their code coverage. The constraints are written in Alloy, a first-order language based on relations. To test a method, given its precondition constraint, we first solve that constraint using the Alloy Analyzer and translate a solution into a test input. Next, we execute the method on that input and build the path condition for the resulting execution path. Then, we run the analyzer on a conjunction of the precondition and a new path condition that represents a previously unexplored path. The solution is translated to a new test input, which triggers the next round of test generation. The iterative execution of Whispec can systematically enumerate inputs that maximize code coverage. Experiments using a variety of data structure implementations from the Java libraries show that our framework generates significantly smaller test suites (while maximizing coverage) than those generated by previous specification-based approaches.

References

[1]
T. Arts and J. Hughes. Erlang/quickcheck. In Ninth International Erlang/OTP User Conference, Nov. 2003.
[2]
B. Beizer. Software Testing Techniques. International Thomson Computer Press, 1990.
[3]
M. Boshernitsan, R. Doong, and A. Savoia. From Daikon to Agitator: lessons and challenges in building a commercial tool for developer testing. In Proc. ACM/SIGSOFT Int. Symp. Software Testing and Analysis, pages 169--180. Portland, Maine, USA, 2006.
[4]
C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In Proc. 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy, July 2002.
[5]
C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: Automatically Generating Inputs of Death. In Proc. of the 13th ACM Conference on Computer and Communications Security (CCS), Alexandria, Virginia, October-November 2006.
[6]
C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Proc. of the 12th International SPIN Workshop on Model Checking of Software, San Francisco, CA, August 2005
[7]
K. Claessen and J. Hughes. Quickcheck: a lightweight tool forrandom testing of haskell programs. In ICFP, pages 268--279, 2000.
[8]
C. Csallner and Y. Smaragdakis. Check 'n' Crash: Combining static checking and testing. In Proc. of the 27th International Conference on Software Engineering (ICSE), St. Louis, MO, May 2005.
[9]
C. Csallner and Y. Smaragdakis. DSD-Crasher: A hybrid analysis tool for bug finding. In Proc. of 2006 International Symposium on Software Testing and Analysis (ISSTA), Portland, Maine, July 2006.
[10]
C. Csallner and Y. Smaragdakis. JCrasher: an automatic robustness tester for Java. Software: Practice and Experience, 34:1025--1050, 2004.
[11]
J. Dolby, M. Vaziri, and F. Tip. Finding Bugs Efficiently with a SAT Solver. In Proc. of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), Dubrovnik, Croatia, September 2007.
[12]
N. Ee'n, and N. Sörensson. An extensible SAT-solver. Theory and Applications of Satisfiability Testing (SAT 2003), Vol 2919:5 of LNCS, Springer, 2004.
[13]
M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, Feb. 2001.
[14]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proc. of ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI), June 2002.
[15]
M. Ganai, L. Zhang, P. Ashar, A. Gupta, and S. Malik. Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In Proc. 39thConference on Design Automation (DAC), Jun. 2002.
[16]
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, January 1997.
[17]
P. Godefroid. Compositional dynamic test generation. In Proc. of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), Nice, France, January 2007.
[18]
P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. of the 2005 ACM SIGPLAN conference on Programming language design and implementation (PLDI), Chicago, IL, June 2005.
[19]
A. Gotlieb, B. Botella, and M. Rueher. Automatic test data generation using constraint solving techniques. In Proc. of the 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), Clearwater Beach, Florida, March 1998.
[20]
N. Gupta, A. P. Mathur, and M. L. Soffa. Generating test data for branch coverage. In Proc. of the 15th International Conference on Automated Software Engineering (ASE), Grenoble, France, September 2000.
[21]
D. Jackson. Object Models as Heap Invirants. In Essays on Programming Methodology, edited by Annabelle McIver and Carroll Morgan. Springer Verlag, 2000.
[22]
D. Jackson. Software Abstractions: logic, language, and analysis. MIT Press, Cambridge, MA, 2006.
[23]
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.
[24]
S. Khurshid, C. Pasareanu and W. Visser. Generalized Symbolic Execution for Model Checking and Testing. The 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland. Apr 2003.
[25]
J. C. King. Symbolic execution and program testing. Communications of the ACM, Volume 19, Issue 7, July 1976.
[26]
R. Majumdar and K. Sen. Hybrid Concolic Testing. In Proc. of the 29th International Conference on Software Engineering (ICSE), Minneapolis, MN, USA, May 2007.
[27]
D. Marinov and S. Khurshid. TestEra: A novel framework for automated testing of Java programs. In Proc. of the 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA, November 2001.
[28]
K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In Proc. of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE), Lisbon, Portugal September, 2005.
[29]
E. Torlak and G. Dennis. Kodkod for Alloy Users. First ACM Alloy Workshop, Portland, Oregon, November 2006.
[30]
E. Torlak and D. Jackson. Kodkod: A Relational Model Finder. The 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Braga, Portugal, March 2007.
[31]
W. Visser, C. S. Pasareanu, S. Khurshid. Test Input Generation with Java PathFinder. In Proc. 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), Boston, MA. July 2004.
[32]
S. Visvanathan and N. Gupta. Generating test data for functions with pointer inputs. In Proc. of the 17th IEEE International Conference on Automated Software Engineering (ASE), September 2002.
[33]
T. Xie, D. Marinov, and D. Notkin. Rostra: A framework for detecting redundant object-oriented unit tests. In Proc. 19th IEEE International Conference on Automated Software Engineering (ASE), September 2004.
[34]
T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proc. of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2005.
[35]
Z. Xu and J. Zhang. A Test Data Generation Tool for Unit Testing of C Programs. In Proc. of the 6th International Conference on Quality Software (QSIC), 2006.
[36]
J. Zhang. Symbolic execution of program paths involving pointers and structure variables. In Proc. of the 4th International Conference on Quality Software (QSIC), 2004
[37]
L. Zhang and S. Malik. The quest for efficient boolean satisfiability solvers. In Proc. 8th Conference on Automated Deduction (CADE), July 2002.

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
LCSD '07: Proceedings of the 2007 Symposium on Library-Centric Software Design
October 2007
125 pages
ISBN:9781605580869
DOI:10.1145/1512762
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 October 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. contracts
  2. first-order logic
  3. software testing
  4. symbolic execution

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)0
Reflects downloads up to 22 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Validation of Formal Models: A Case StudyThe Practice of Formal Methods10.1007/978-3-031-66673-5_15(292-313)Online publication date: 4-Sep-2024
  • (2022)ATR: template-based repair for Alloy specificationsProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3533767.3534369(666-677)Online publication date: 18-Jul-2022
  • (2021)Model Finding for ExplorationProtocols, Strands, and Logic10.1007/978-3-030-91631-2_9(156-174)Online publication date: 19-Nov-2021
  • (2020)AlloyMC: Alloy meets model countingProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3417938(1541-1545)Online publication date: 8-Nov-2020
  • (2019)Efficient test generation guided by field coverage criteriaProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00019(91-101)Online publication date: 10-Nov-2019
  • (2019)A First Step in the Translation of Alloy to CoqFormal Methods and Software Engineering10.1007/978-3-030-32409-4_28(455-469)Online publication date: 28-Oct-2019
  • (2018)CompoSAT: Specification-Guided Coverage for Model FindingFormal Methods10.1007/978-3-319-95582-7_34(568-587)Online publication date: 12-Jul-2018
  • (2016)Field-exhaustive testingProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950336(908-919)Online publication date: 1-Nov-2016
  • (2013)Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT SolvingProceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation10.1109/ICST.2013.46(21-30)Online publication date: 18-Mar-2013
  • (2013)Applications and extensions of Alloy: past, present and futureMathematical Structures in Computer Science10.1017/S096012951200029123:4(915-933)Online publication date: 8-Jul-2013
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media