Theorem-Prover-Based Testing: HOL-TestGen

Theorem-prover based testing combines testing and verification: tests are derived from a formal specification (or model, i.e., it is a model-based testing technique) proof techniques. HOL-TestGen is a theorem-prover based testing environment on top of Isabelle.

HOL-TestGen: a theorem-prover based testing environment

The main result of our work in the area of theorem-prover based testing [1] is the HOL-TestGen [2] system. HOL-TestGen is jointly developed by the Software Assurance & Security Research Team at the University of Exeter, UK and the Verified Algorithms, Languages and Systems team at the LRI (CNRS and University of Paris-Sud), France.

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

As a unique feature, HOL-TestGen supports the end-to-end life-cycle of formal system testing and verification: from a formal specification that can be formally verified, to formally verified specification transformation (model-transformation), to abstract test case generation, concrete test data generation, to the generation and execution of test scrips that test a real system under test.

HOL-TestGen has been used in large case studies in various application domains, including conformance testing of security properties (e.g., firewall policies [3] and health-care-specific access control systems [4]).

HOL-TestGen is free software; you can redistribute it and/or modify it under the terms of a BSD-style license.

Important Publications

[1]
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.
[2]
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.
[3]
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.
[4]
A. D. Brucker, L. Brügger, P. Kearney, and B. Wolff, “An approach to modular and testable security models of real-world health-care applications,” in ACM symposium on access control models and technologies (SACMAT), 2011, pp. 133–142. doi: 10.1145/1998441.1998461.
[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.