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 Sheffield, 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.
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 licence. For more information, please visit the HOL-TestGen home page.

Important Publications

1. Brucker, A. D. and Wolff, B. “On Theorem Prover-Based TestingFormal Aspects of Computing 25, no. 5 (2013): 683–721. doi:10.1007/s00165-012-0222-y, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012

2. Brucker, A. D. and Wolff, B.“: An Interactive Test-Case Generation FrameworkFundamental approaches to software engineering (fase09) (2009): 417–420. doi:10.1007/978-3-642-00593-0_28, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009

3. Brucker, A. D., Brügger, L., and Wolff, B. “Formal Firewall Conformance Testing: An Application of Test and Proof TechniquesSoftware Testing, Verification & Reliability (STVR) 25, no. 1 (2015): 34–71. doi:10.1002/stvr.1544, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014

4. Brucker, A. D., Brügger, L., Kearney, P., and Wolff, B. “An Approach to Modular and Testable Security Models of Real-World Health-Care ApplicationsACM symposium on access control models and technologies (sacmat) (2011): 133–142. doi:10.1145/1998441.1998461, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-model-based-2011

5. Brucker, A. D., Brügger, L., and Wolff, B. “/Fw: An Environment for Specification-Based Firewall Conformance TestingInternational colloquium on theoretical aspects of computing (ictac) (2013): 112–121. doi:10.1007/978-3-642-39718-9_7, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-fw-2013