Firewalls are a cornerstone of todays security infrastructure for networks. Their configuration, implementing a firewall policy,
is inherently complex, hard to understand, and difficult to validate.
We present a substantial case study performed with the model-based testing tool TestGen. Based on a formal model of firewalls and their policies in higher-order logic hol, we first present a derived theory for simplifying policies. We discuss different test plans for test specifications. Finally,
we show how to integrate these issues to a domain-specific firewall testing tool holTestGen/fw.
Keywords Security Testing - Model-based Testing - Firewall - Conformance Testing