Test-Sequence Generation with HOL-TestGen – With an Application to Firewall Testing

By Achim D. Brucker and Burkhart Wolff.

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. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs.

Although originally designed for black-box unit-tests, HOL-TestGen’s underlying logic and deduction engine is powerful enough to be used in test-sequence generation, too.

We develop the theory for test-sequence generation with HOL-TestGen and describe its use in a substantial case-study in the field of computer security, namely the black-box test of configured firewalls.

Keywords:
Security, Model-Based Testing, Specification-Based Testing, Firewall Testing

Obsoleted by:
This publication has been obsoleted by the following publication:
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/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Test-sequence generation with HOL-TestGen – with an application to firewall testing,” in TAP 2007: Tests and proofs, B. Meyer and Y. Gurevich, Eds. Heidelberg: Springer-Verlag, 2007, pp. 149–168. doi: 10.1007/978-3-540-73770-4_9. Author copy: http://logicalhacking.com/publications/brucker.ea-test-sequence-2007/

BibTeX
@InCollection{ brucker.ea:test-sequence:2007,
  abstract    = {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. Second, the test cases are analyzed for ground
                 instances (the test data) satisfying the constraints of the
                 test cases. Particular emphasis is put on the control of
                 explicit test hypotheses which can be proven over concrete
                 programs.
                 
                 Although originally designed for black-box unit-tests,
                 HOL-TestGen's underlying logic and deduction engine is
                 powerful enough to be used in test-sequence generation, too.
                 
                 We develop the theory for test-sequence generation with
                 HOL-TestGen and describe its use in a substantial case-study
                 in the field of computer security, namely the black-box test
                 of configured firewalls.},
  keywords    = {Security, Model-Based Testing, Specification-Based Testing,
                 Firewall Testing},
  location    = {Zurich},
  author      = {Achim D. Brucker and Burkhart Wolff},
  booktitle   = {{TAP} 2007: Tests And Proofs},
  language    = {USenglish},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  number      = {4454},
  editor      = {Bertrand Meyer and Yuri Gurevich},
  title       = {Test-Sequence Generation with {HOL-TestGen} -- With an
                 Application to Firewall Testing},
  obsoletedby = {brucker.ea:theorem-prover:2012},
  areas       = {security, formal methods, software},
  year        = {2007},
  doi         = {10.1007/978-3-540-73770-4_9},
  pages       = {149--168},
  isbn        = {978-3-540-73769-8},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-test-sequence-2007/}},
}