Symbolic Test-generation in HOL-TESTGEN/CirTA A Case Study

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments

    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.

    Cited by
Get Citation

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

Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
  • Received:
  • Revised:
  • Adopted:
  • Online: August 26,2015
  • Published: