Added HOL-TestGen reference.
This commit is contained in:
parent
73bc5df9fc
commit
5d71be04f7
|
@ -28,7 +28,7 @@ to express access control policies on the network level using a
|
||||||
combinator-based language that is close to textbook-style
|
combinator-based language that is close to textbook-style
|
||||||
specifications of firewall rules. To actually test the implementation
|
specifications of firewall rules. To actually test the implementation
|
||||||
as well as the configuration of a firewall, we use
|
as well as the configuration of a firewall, we use
|
||||||
HOL-TestGen~\cite{brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012}
|
HOL-TestGen~\cite{brucker.ea:interactive:2005,brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012}
|
||||||
to generate test cases that can be used to validate the compliance of
|
to generate test cases that can be used to validate the compliance of
|
||||||
real network middleboxes (e.g., firewalls, routers). In this document,
|
real network middleboxes (e.g., firewalls, routers). In this document,
|
||||||
we focus on the Isabelle formalization of network access control
|
we focus on the Isabelle formalization of network access control
|
||||||
|
|
|
@ -397,4 +397,40 @@
|
||||||
isbn = {978-1-4503-0688-1},
|
isbn = {978-1-4503-0688-1},
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@InCollection{ brucker.ea:interactive:2005,
|
||||||
|
keywords = {symbolic test case generations, black box testing, white
|
||||||
|
box testing, theorem proving, interactive testing},
|
||||||
|
abstract = {\testgen is a test environment for specification-based
|
||||||
|
unit testing build upon the proof assistant Isabelle/\acs{hol}\@.
|
||||||
|
While there is considerable skepticism with regard to
|
||||||
|
interactive theorem provers in testing communities, we
|
||||||
|
argue that they are a natural choice for (automated)
|
||||||
|
symbolic computations underlying systematic tests. This
|
||||||
|
holds in particular for the development on non-trivial
|
||||||
|
formal test plans of complex software, where some parts of
|
||||||
|
the overall activity require inherently guidance by a test
|
||||||
|
engineer. In this paper, we present the underlying methods
|
||||||
|
for both black box and white box testing in interactive
|
||||||
|
unit test scenarios. \testgen can also be understood as
|
||||||
|
a unifying technical and conceptual framework for
|
||||||
|
presenting and investigating the variety of unit test
|
||||||
|
techniques in a logically consistent way. },
|
||||||
|
location = {Edinburgh},
|
||||||
|
author = {Achim D. Brucker and Burkhart Wolff},
|
||||||
|
booktitle = {Formal Approaches to Testing of Software},
|
||||||
|
language = {USenglish},
|
||||||
|
publisher = pub-springer,
|
||||||
|
series = s-lncs,
|
||||||
|
number = 3997,
|
||||||
|
doi = {10.1007/11759744_7},
|
||||||
|
isbn = {3-540-25109-X},
|
||||||
|
editor = {Wolfgang Grieskamp and Carsten Weise},
|
||||||
|
project = {\acs{csfmdos}},
|
||||||
|
title = {Interactive Testing using \testgen},
|
||||||
|
classification= {workshop},
|
||||||
|
areas = {formal methods, software},
|
||||||
|
categories = {holtestgen},
|
||||||
|
year = 2005,
|
||||||
|
public = {yes},
|
||||||
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue