HOL-TestGen/CirTA is a theorem-prover based test generation environment for speci cations written in Circus, a process-algebraic speci cation language in the tradition of CSP. HOL-TestGen/CirTA is based on a formal embedding of its semantics in Isabelle/HOL, allowing to derive rules over speci cation constructs in a logically safe way. Beyond the derivation of algebraic laws and calculi for process re nement, the originality of HOL-TestGen/ CirTA consists in an entire derived theory for the generation of symbolic test-traces, including optimized rules for test-generation as well as rules for symbolic execution. The deduction process is automated by Isabelle tactics, allowing to protract the state-space explosion resulting from blind enumeration of data. The implementation of test-generation procedures in CirTA is completed by an integrated tool chain that transforms the initial Circus speci cation of a system into a set of equivalence classes (or "symbolic tests"), which were compiled to conventional JUnit test-drivers. This paper describes the novel tool-chain based on prior theoretical work on semantics and test-theory and attempts an evaluation via a medium-sized case study performed on a component of a real-world safety-critical medical monitoring system written in Java. We provide experimental measurements of the kill-capacity of implementation mutants.
Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff. Symbolic Test-generation in HOL-TESTGEN/CirTA A Case Study. International Journal of Software and Informatics, 2015,9(2):177~203Copy