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: 3266
Download times: 1596
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

 

 

more>>  
Visitor:3203579
Top Paper  |  E-mail Alert  |  Publication Ethics  |  New Version

© Copyright by Institute of Software, the Chinese Academy of Sciences
京ICP备05046678号-5

京公网安备 11040202500065号