@InProceedings{ feliachi.ea:circus:2013,
abstract = {Formal specifications provide strong bases for testing and
bring powerful techniques and technologies. Expressive
formal specification languages combine large data domain
and behavior. Thus, symbolic methods have raised particular
interest for test generation techniques. Integrating formal
testing in proof environments such as Isabelle/HOL is
referred to as "theorem-prover based testing".
Theorem-prover based testing can be adapted to a specific
specification language via a representation of its formal
semantics, paving the way for specific support of its
constructs. The main challenge of this approach is to
reduce the gap between pen-and-paper semantics and formal
mechanized theories. In this paper we consider testing
based on the Circus specification language. This language
integrates the notions of states and of complex data in a
Z-like fashion with communicating processes inspired from
CSP. We present a machine-checked formalization in
Isabelle/HOL of this language and its testing theory. Based
on this formal representation of the semantics we revisit
the original associated testing theory. We discovered
unforeseen simplifications in both definitions and symbolic
computations. The approach lends itself to the construction
of a tool, that directly uses semantic definitions of the
language as well as derived rules of its testing theory,
and thus provides some powerful symbolic computation
machinery to seamlessly implement them both in a technical
environment. },
keywords = {symbolic test case generations, black box testing, theorem
proving, network security, firewall testing, conformance
testing},
location = {Wellington},
author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Makarius
Wenzel and Burkhart Wolff},
title = {The Circus Testing Theory Revisited in Isabelle/HOL},
booktitle = {ICFEM},
year = {2013},
pages = {131--147},
doi = {10.1007/978-3-642-41202-8_10},
editor = {Lindsay Groves and Jing Sun},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8144},
isbn = {978-3-642-41201-1},
categories = {holtestgen},
public = yes,
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-Circus-testing.pdf},
url = {https://www.brucker.ch/bibliography/abstract/feliachi.ea-circus-2013}
}