Article

Interactive testing with HOL-TestGen

Authors:

Achim D. Brucker,

Burkhart WolffAuthors Info & Claims

FATES'05: Proceedings of the 5th international conference on Formal Approaches to Software Testing

Pages 87 - 102

https://doi.org/10.1007/11759744_7

Published: 11 July 2005 Publication History

Abstract

HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant Isabelle/HOL . While there is considerable skepticism with regard to interactive theorem provers in testing communities, we argue that they are a natural choice for (automated) symbolic computations underlying systematic tests. This holds in particular for the development on non-trivial formal test plans of complex software, where some parts of the overall activity require inherently guidance by a test engineer. In this paper, we present the underlying methods for both black box and white box testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit test techniques in a logically consistent way.

References

[1]

HOL-TestGen. http://www.brucker.ch/projects/hol-testgen/.

Google Scholar

[2]

IMP. http://isabelle.in.tum.de/library/HOL/IMP/Denotation.html.

Google Scholar

[3]

P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, Orlando, May 1986.

Digital Library

Google Scholar

[4]

C. Boyapati, S. Khurshid, and D. Marinov. Korat: automated testing based on Java predicates. In Proceedings of the international symposium on Software testing and analysis, pages 123-133, 2002.

Digital Library

Google Scholar

[5]

A. D. Brucker and B. Wolff. HOL-TestGen 1.0.0 user guide. Technical Report 482, ETH Zrich, Apr. 2005.

Google Scholar

[6]

A. D. Brucker and B. Wolff. Symbolic test case generation for primitive recursive functions. In J. Grabowski and B. Nielsen, editors, Formal Approaches to Testing of Software, number 3395 in Lecture Notes in Computer Science, pages 16-32. Springer-Verlag, Linz, 2005.

Digital Library

Google Scholar

[7]

A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940.

Crossref

Google Scholar

[8]

W. Grieskamp, N. Tillmann, and M. Veanes. Instrumenting scenarios in a model-driven development environment. Information and Software Technology, 46(15):1027-1036, 2004.

Crossref

Google Scholar

[9]

T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171-186, 1998.

Digital Library

Google Scholar

[10]

T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

Google Scholar

[11]

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engg., 10(2):203-232, 2003.

Digital Library

Google Scholar

[12]

M. M. Wenzel. Isabelle/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, TUMünchen, München, Feb. 2002.

Google Scholar

[13]

G. Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993.

Digital Library

Google Scholar

Cited By

View all

Sachtleben R(2020)An Executable Mechanised Formalisation of an Adaptive State Counting AlgorithmTesting Software and Systems10.1007/978-3-030-64881-7_15(236-254)Online publication date: 9-Dec-2020
https://dl.acm.org/doi/10.1007/978-3-030-64881-7_15
Sachtleben RHierons RHuang WPeleska J(2019)A Mechanised Proof of an Adaptive State Counting AlgorithmTesting Software and Systems10.1007/978-3-030-31280-0_11(176-193)Online publication date: 15-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31280-0_11
Carlier MDubois CGotlieb A(2012)A first step in the design of a formally verified constraint-based testing toolProceedings of the 6th international conference on Tests and Proofs10.1007/978-3-642-30473-6_5(35-50)Online publication date: 31-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-30473-6_5
Show More Cited By

Recommendations

hol-TestGen
FASE '09: Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009

We present <Emphasis Type="SmallCaps">hol-TestGen</Emphasis> , an extensible test environment for specification-based testing build upon the proof assistant Isabelle. <Emphasis Type="SmallCaps">hol-TestGen</Emphasis> leverages the semi-automated ...
Test-sequence generation with Hol-TestGen with an application to firewall testing
TAP'07: Proceedings of the 1st international conference on Tests and proofs

HOL-TESTGEN is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. Its method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called ...
Verifying Test-Hypotheses

hol-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/hol. The hol-TestGen method is two-staged: first, the original formula, called test specification, is partitioned into test cases by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

FATES'05: Proceedings of the 5th international conference on Formal Approaches to Software Testing

July 2005

217 pages

ISBN:3540344543

Editors:
Wolfgang Grieskamp
Microsoft Research, Redmond, WA
,
Carsten Weise
Ericsson Deutschland GmbH, Herzogenrath, WA, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 July 2005

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sachtleben R(2020)An Executable Mechanised Formalisation of an Adaptive State Counting AlgorithmTesting Software and Systems10.1007/978-3-030-64881-7_15(236-254)Online publication date: 9-Dec-2020
https://dl.acm.org/doi/10.1007/978-3-030-64881-7_15
Sachtleben RHierons RHuang WPeleska J(2019)A Mechanised Proof of an Adaptive State Counting AlgorithmTesting Software and Systems10.1007/978-3-030-31280-0_11(176-193)Online publication date: 15-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31280-0_11
Carlier MDubois CGotlieb A(2012)A first step in the design of a formally verified constraint-based testing toolProceedings of the 6th international conference on Tests and Proofs10.1007/978-3-642-30473-6_5(35-50)Online publication date: 31-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-30473-6_5
Zimmerman DNagmoti R(2010)JMLUnitProceedings of the 2010 international conference on Formal verification of object-oriented software10.5555/1949303.1949316(183-197)Online publication date: 28-Jun-2010
https://dl.acm.org/doi/10.5555/1949303.1949316
Engel CHähnle R(2007)Generating unit tests from formal proofsProceedings of the 1st international conference on Tests and proofs10.5555/1776119.1776129(169-188)Online publication date: 12-Feb-2007
https://dl.acm.org/doi/10.5555/1776119.1776129
Brucker AWolff B(2007)Test-sequence generation with Hol-TestGen with an application to firewall testingProceedings of the 1st international conference on Tests and proofs10.5555/1776119.1776128(149-168)Online publication date: 12-Feb-2007
https://dl.acm.org/doi/10.5555/1776119.1776128
Beckert BHoare THahnle RSmith DGreen CRanise STinelli CBall TRajamani S(2006)Intelligent Systems and Formal Methods in Software EngineeringIEEE Intelligent Systems10.1109/MIS.2006.11721:6(71-81)Online publication date: 1-Nov-2006
https://dl.acm.org/doi/10.1109/MIS.2006.117

Abstract

References

Cited By

Recommendations

hol-TestGen

Test-sequence generation with Hol-TestGen with an application to firewall testing

Verifying Test-Hypotheses

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations