| Symbolic Test-generation in HOL-TESTGEN/CirTA A Case Study |
| Download PDF |
| 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~203 |
| Hits: 2391 |
| Download times: 864 |
|
|
| Abstract: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. |
| keywords:symbolic test-case generations black box testing theorem proving model-based testing JUnit |
| View Full Text View/Add Comment Download reader |
|
|
|
