Article

An empirical framework for comparing effectiveness of testing and property-based formal analysis

Authors:

Jeremy S. Bradbury,

James R. Cordy,

Juergen DingelAuthors Info & Claims

PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

Pages 2 - 5

https://doi.org/10.1145/1108792.1108795

Published: 05 September 2005 Publication History

Abstract

Today, many formal analysis tools are not only used to provide certainty but are also used to debug software systems - a role that has traditional been reserved for testing tools. We are interested in exploring the complementary relationship as well as tradeoffs between testing and formal analysis with respect to debugging and more specifically bug detection. In this paper we present an approach to the assessment of testing and formal analysis tools using metrics to measure the quantity and efficiency of each technique at finding bugs. We also present an assessment framework that has been constructed to allow for symmetrical comparison and evaluation of tests versus properties. We are currently beginning to conduct experiments and this paper presents a discussion of possible outcomes of our proposed empirical study.

References

[1]

P. Anderson. CodeSurfer/Path Inspector. In Proc. of the IEEE Int. Conf. on Software Maintenance (ICSM04), Sept. 2004.

Digital Library

[2]

J. H. Andrews, L. C. Briand, and Y. Labiche. Is mutation an appropriate tool for testing experiments? In Proc. of ICSE 2005, pages 402--411, 2005.

Digital Library

[3]

T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. of Symp. on Principles of Programming Languages (POPL 2002), pages 1--3, Jan. 2002.

Digital Library

[4]

S. S. Brilliant and J. C. Knight. Empirical research in software engineering: a workshop. SIGSOFT Software Engineering Notes, 24(3):44--52, 1999.

Digital Library

[5]

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proc. of ICSE'99, pages 411--420, May 1999.

Digital Library

[6]

M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Trans. on Soft. Eng., 27(2):1--25, Feb. 2001.

Digital Library

[7]

G. Hamon, L. de Moura, and J. Rushby. Generating efficient test sets with a model checker. In Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM'04), pages 261--270, Sept. 2004.

Digital Library

[8]

C. A. R. Hoare. Assertions: A personal perspective. IEEE Annals of the History of Computing, 25(2), Apr.-Jun. 2003.

Digital Library

[9]

Y. Hoskote, T. Kam, P. Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proc. of the Conference on Design Automation (DAC 1999), pages 300--305, Jun. 1999.

Digital Library

[10]

M. Hutchins, H. Foster, T. Goradia, and T. Ostrand. Experiments on the effectiveness of dataflow- and controlflow-based test adequacy criteria. In Proc. of ICSE'94, pages 191--200, May 1994.

Digital Library

[11]

N. Juristo, A. M. Moreno, and S. Vegas. Towards building a solid empirical body of knowledge in testing techniques. SIGSOFT Software Engineering Notes, 29(5):1--4, 2004.

Digital Library

[12]

S. Lu, Z. Li, F. Qin, L. Tan, P. Zhou, and Y. Zhou. Bugbench: Benchmarks for evaluating bug detection tools. In Proc. of the Work. on the Evaluation of Software Defect Detection Tools, June 2005.

[13]

Robby, M. B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular software model checking framework. In Proc. of ESEC/FSE-11, pages 267--276, Sept. 2003.

Digital Library

[14]

G. Rothermel and M. J. Harrold. Empirical studies of a safe regression test selection technique. IEEE Trans. on Soft. Eng., 25(6):401--419, Jun. 1998.

Digital Library

[15]

J. Rushby. Disappearing formal methods. In Proc. of the High-Assurance Systems Engineering Symp. (HASE'00), Nov. 2000.

[16]

H. Sutter. The free lunch is over: A fundamental turn toward concurrency in software. Dr. Dobb's Journal, 30(3), Mar. 2005.

[17]

J. Yang and D. Evans. Dynamically inferring temporal properties. In Proc. of the ACM SIGPLAN-SIGSOFT Work. on Program Analysis for Software Tools and Engineering (PASTE 2004), Jun. 2004.

Digital Library

Cited By

Namin AXue XRosas OSharma P(2015)MuRankerSoftware Testing, Verification & Reliability10.1002/stvr.154225:5-7(572-604)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.1002/stvr.1542
Kusano MWang CDenney EBultan TZeller A(2013)CCmutatorProceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2013.6693142(722-725)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1109/ASE.2013.6693142
Namin AKakarla SDwyer MTip F(2011)The use of mutation in testing experiments and its sensitivity to external threatsProceedings of the 2011 International Symposium on Software Testing and Analysis10.1145/2001420.2001461(342-352)Online publication date: 17-Jul-2011
https://dl.acm.org/doi/10.1145/2001420.2001461
Show More Cited By

Index Terms

An empirical framework for comparing effectiveness of testing and property-based formal analysis

Recommendations

An empirical framework for comparing effectiveness of testing and property-based formal analysis

Today, many formal analysis tools are not only used to provide certainty but are also used to debug software systems - a role that has traditional been reserved for testing tools. We are interested in exploring the complementary relationship as well as ...
To Kill a Mutant: An Empirical Study of Mutation Testing Kills
ISSTA 2023: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis

Mutation testing has been used and studied for over four decades as a method to assess the strength of a test suite. This technique adds an artificial bug (i.e., a mutation) to a program to produce a mutant, and the test suite is run to determine if ...
Mitigating the effects of flaky tests on mutation testing
ISSTA 2019: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

Mutation testing is widely used in research as a metric for evaluating the quality of test suites. Mutation testing runs the test suite on generated mutants (variants of the code under test), where a test suite kills a mutant if any of the tests fail ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering

September 2005

118 pages

ISBN:1595932399

DOI:10.1145/1108792

Editors:
Michael Ernst
MIT
,
Thomas Jensen
CNRS

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 1
January 2006
203 pages
ISSN:0163-5948
DOI:10.1145/1108768
Issue’s Table of Contents

Copyright © 2005 ACM.

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: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PASTE05

Sponsor:

PASTE05: PASTE '05 - ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering

September 5 - 6, 2005

Lisbon, Portugal

Acceptance Rates

Overall Acceptance Rate 57 of 159 submissions, 36%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
412
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Namin AXue XRosas OSharma P(2015)MuRankerSoftware Testing, Verification & Reliability10.1002/stvr.154225:5-7(572-604)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.1002/stvr.1542
Kusano MWang CDenney EBultan TZeller A(2013)CCmutatorProceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2013.6693142(722-725)Online publication date: 11-Nov-2013
https://dl.acm.org/doi/10.1109/ASE.2013.6693142
Namin AKakarla SDwyer MTip F(2011)The use of mutation in testing experiments and its sensitivity to external threatsProceedings of the 2011 International Symposium on Software Testing and Analysis10.1145/2001420.2001461(342-352)Online publication date: 17-Jul-2011
https://dl.acm.org/doi/10.1145/2001420.2001461
Baharom SShukur Z(2011)An experimental assessment of module documentation-based testingInformation and Software Technology10.1016/j.infsof.2011.01.00553:7(747-760)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1016/j.infsof.2011.01.005
Jürjens JReiß DTrachtenherz D(2008)Model-Based Quality Assurance of Automotive SoftwareProceedings of the 11th international conference on Model Driven Engineering Languages and Systems10.1007/978-3-540-87875-9_59(858-873)Online publication date: 28-Sep-2008
https://dl.acm.org/doi/10.1007/978-3-540-87875-9_59
Wojcicki MStrooper P(2007)An Iterative Empirical Strategy for the Systematic Selection of a Combination of Verification and Validation TechnologiesProceedings of the 5th International Workshop on Software Quality10.1109/WOSQ.2007.4Online publication date: 20-May-2007
https://dl.acm.org/doi/10.1109/WOSQ.2007.4
Bradbury JCordy JDingel J(2006)ExMAnProceedings of the Second Workshop on Mutation Analysis10.1109/MUTATION.2006.5Online publication date: 7-Nov-2006
https://dl.acm.org/doi/10.1109/MUTATION.2006.5
Zhang HBradbury JCordy JDingel J(2006)Using source transformation to test and model check implicit-invocation systemsScience of Computer Programming10.1016/j.scico.2006.04.00862:3(209-227)Online publication date: 15-Oct-2006
https://dl.acm.org/doi/10.1016/j.scico.2006.04.008
Namin AXue XRosas OSharma P(2015)MuRankerSoftware Testing, Verification & Reliability10.1002/stvr.154225:5-7(572-604)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.1002/stvr.1542
Jenkins WVilkomir SBallance W(2010)Fault Evaluator: A tool for experimental investigation of effectiveness in software testing2010 IEEE International Conference on Progress in Informatics and Computing10.1109/PIC.2010.5688000(1077-1083)Online publication date: Dec-2010
https://doi.org/10.1109/PIC.2010.5688000
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents