The Circus Testing Theory Revisited in Isabelle/HOL

by Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, and Burkhart Wolff

Cover for feliachi.ea:circus:2013.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
Categories:
Documents: (full text as PDF file)

QR Code for feliachi.ea:circus:2013.Please cite this article as follows:
Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, and Burkhart Wolff. The Circus Testing Theory Revisited in Isabelle/HOL. In ICFEM. Lecture Notes in Computer Science, 8144, pages 131-147, Springer, 2013.
Keywords: symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-41202-8_10) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@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.},
author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Makarius Wenzel and Burkhart Wolff},
booktitle = {ICFEM},
doi = {10.1007/978-3-642-41202-8_10},
editor = {Lindsay Groves and Jing Sun},
isbn = {978-3-642-41201-1},
keywords = {symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing},
location = {Wellington},
pages = {131--147},
pdf = {http://www.lri.fr/~wolff/papers/conf/2013-Circus-testing.pdf},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {The Circus Testing Theory Revisited in Isabelle/HOL},
url = {https://www.brucker.ch/bibliography/abstract/feliachi.ea-circus-2013},
volume = {8144},
year = {2013},
}