Abstract:


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


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.