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

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:test-sequence:2007.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.

Schlüsselwörter: security, model-based testing, specification-based testing, firewall testing
Kategorien: , ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:test-sequence:2007.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science (4454), pages 149-168, Springer-Verlag, 2007.
Schlüsselwörter: security, model-based testing, specification-based testing, firewall testing
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-73770-4_9) (Share article on LinkedIn. Share article on CiteULike.)

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.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {{TAP} 2007: Tests And Proofs},
doi = {10.1007/978-3-540-73770-4_9},
editor = {Bertrand Meyer and Yuri Gurevich},
isbn = {978-3-540-73769-8},
keywords = {security, model-based testing, specification-based testing, firewall testing},
language = {USenglish},
location = {Zurich},
number = {4454},
pages = {149--168},
pdf = {https://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf},
project = {CSFMDOS},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Test-Sequence Generation with {HOL-TestGen} -- With an Application to Firewall Testing},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007},
year = {2007},
}