HOL-TestGen
[archived]

HOL-TestGen is a is a test case generator for specification based unit testing. HOL-TestGen is built on top of the specfication and theorem proving environment Isabelle. As a theorem-prover based testing tool, it combines testing and verification: tests are derived from a formal specification (or model, i.e., it is a model-based testing technique) proof techniques.

Testing a simple sorting algorithm for lists using HOL-TestGen.

HOL-TestGen allows one to

  • write test specifications in Higher-order logics (HOL)
  • (semi-) automatically partition the input space, resulting in abstract test cases
  • automatically select concrete test data
  • automatically generate test scripts (in SML)
  • using a foreign language interface, implementations in arbitrary languages (e.g. C) can be tested.

HOL-TestGen is free software; you can redistribute it and/or modify it under the terms of a BSD-style licence. HOL-TestGen 1.5 has been deposited in the Agency for the protection of programs (APP) IDDN.FR.001.220032.000.S.A.2011.000.10000 (Signed Paris, 3.6. 2011).

Releases §

Important Publications §

[1]
A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” in Fundamental approaches to software engineering (FASE09), M. Chechik and M. Wirsing, Eds. Heidelberg: Springer-Verlag, 2009, pp. 417–420. doi: 10.1007/978-3-642-00593-0_28. Author copy: http://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/
[2]
A. D. Brucker, M. P. Krieger, D. Longuet, and B. Wolff, “A specification-based test case generation method for UML/OCL,” in MoDELS workshops, J. Dingel and A. Solberg, Eds. Heidelberg: Springer-Verlag, 2010, pp. 334–348. doi: 10.1007/978-3-642-21210-9_33. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.. Author copy: http://logicalhacking.com/publications/brucker.ea-ocl-testing-2010/
[3]
A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Aspects of Computing (FAC), vol. 25, no. 5, pp. 683–721, 2013, doi: 10.1007/s00165-012-0222-y. Author copy: http://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/
[4]
A. D. Brucker, L. Brügger, and B. Wolff, “Formal firewall conformance testing: An application of test and proof techniques,” Software Testing, Verification & Reliability (STVR), vol. 25, no. 1, pp. 34–71, 2015, doi: 10.1002/stvr.1544. Author copy: http://logicalhacking.com/publications/brucker.ea-formal-fw-testing-2014/
[5]
A. D. Brucker, L. Brügger, and B. Wolff, “HOL-TestGen/FW: An environment for specification-based firewall conformance testing,” in International colloquium on theoretical aspects of computing (ICTAC), Z. Liu, J. Woodcock, and H. Zhu, Eds. Heidelberg: Springer-Verlag, 2013, pp. 112–121. doi: 10.1007/978-3-642-39718-9_7. Author copy: http://logicalhacking.com/publications/brucker.ea-hol-testgen-fw-2013/
[6]
A. D. Brucker, O. Havle, Y. Nemouchi, and B. Wolff, “Testing the IPC protocol for a real-time operating system,” in Working conference on verified software: Theories, tools, and experiments, A. Gurfinkel and S. A. Seshia, Eds. Heidelberg: Springer-Verlag, 2015. doi: 10.1007/978-3-319-29613-5_3. Author copy: http://logicalhacking.com/publications/brucker.ea-ipc-testing-2015/
[7]
A. D. Brucker and B. Wolff, “Monadic sequence testing and explicit test-refinements,” in TAP 2016: Tests and proofs, B. K. Aichernig and C. A. Furia, Eds. Heidelberg: Springer-Verlag, 2016. doi: 10.1007/978-3-319-41135-4_2. Author copy: http://logicalhacking.com/publications/brucker.ea-monadic-sequence-testing-2016/