Theorem-Prover-Based Testing

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. Author copy: http://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/
[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. Author copy: http://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/
[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. Author copy: http://logicalhacking.com/publications/brucker.ea-formal-fw-testing-2014/
[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. Author copy: http://logicalhacking.com/publications/brucker.ea-model-based-2011/
[5]
A. D. Brucker, A. Feliachi, Y. Nemouchi, and B. Wolff, “Test program generation for a microprocessor: A case-study,” in TAP 2013: Tests and proofs, L. Viganò and M. Veanes, Eds. Heidelberg: Springer-Verlag, 2013, pp. 76–95. doi: 10.1007/978-3-642-38916-0_5. Author copy: http://logicalhacking.com/publications/brucker.ea-test-program-generation-2013/
[6]
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/
[7]
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/
[8]
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/
[9]
A. D. Brucker and M. Herzberg, “Formalizing (web) standards: An application of test and proof,” in TAP 2018: Tests and proofs, C. Dubois and B. Wolff, Eds. Heidelberg: Springer-Verlag, 2018, pp. 159–166. doi: 10.1007/978-3-319-92994-1_9. Author copy: http://logicalhacking.com/publications/brucker.ea-standard-compliance-testing-2018/