@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},
  project	= {CSFMDOS},
  title		= {Test-Sequence Generation with {HOL-TestGen} -- With an
		  Application to Firewall Testing },
  categories	= {holtestgen},
  classification= {conference},
  areas		= {security, formal methods, software},
  public	= {yes},
  year		= {2007},
  doi		= {10.1007/978-3-540-73770-4_9},
  pages		= {149--168},
  isbn		= {978-3-540-73769-8},
  pdf		= {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007}
		  
}