Techniques for the automated generation of test-cases — be it from specifications in form of pre- and postconditions, from transition systems or from annotated programs — suffer from state-space explosion similarly to model-checking techniques. One possible anwer to the challenge is to use symbolic representations of models, their normal forms, symbolic states, the resulting test-cases (partitions of test-data) and constraint-solving techniques for test-data selection.

##

Aims and Scope :

The proof-based testing paradigm is described by the goal to transform specifications as long as possible **abstractly** and normalizing them in an automated deduction process specific to the problem domain. Proof-based testing depends on the following prerequisites:

- Logical representations are required for the various specification languages, presenting the semantics in a formal, unambiguous way, in order to allow for verified transformation rules and normalization processes.
- Proof-environments have to be adapted in order to represent test-case generation processes as symbolic evaluation and problem-specific normalization.
- Constraint-solvers and random-exploration methods have to be integrated into the process, in particular for the test-data selection.
- New technologies such as fine-grained parallelization have to be integrated in the underlying symbolic computing processes in order to leverage test-case generation for large models.
- New forms of test-driver generations have to be developed in order to improve the applicability of the approach to more application domains.

##

Main achievements

- Ad 1.) we developed various semantic theories (so called "shallow embeddings") for programming and specification languages in Isabelle/HOL. Examples are UML/OCL, Z, CSP, Circus, core-languages of C like Boogie, or UPF (a special purpose language to describe security policies) in Isabelle/HOL. Rule-sets derived from these theories can be used for specification normalization, which are a pre-requisite for (efficient) test-case generation techniques.
- Ad 2), we developed the environment HOL-TestGen, (built as a kind of "plugin" in Isabelle/HOL), which provides an infrastructure for test-case generation by decomposing specifications or annotated programs into classes of data (characterized by constraint-systems or path-conditions), for constraint-solving based test-data selection and for the generation of efficient test-drivers.
- Ad 3) we integrated SMT solvers like Z3, in particular the counter-example generation facility into HOL-TestGen; a future integration of uniform random-distribution techniques such as Rukia is another line of future research.
- Ad 4), we aim to integrate parallelism into the kernel of Isabelle and similar systems in order to profit from new hardware-trends and the fact, that normal-from computations in test-case generation procedures are highly suited for parallelization.
- Ad 5), we developed for example specific test-drivers for web-service tests, future developments can also include the generation of runtime-testers for temporal properties.

## People

- Burkhart Wolff
- Marie-Claude Gaudel
- Delphine Longuet
- Matthias Krieger (- 2012)
- Abdou Feliachi
- Yakoub Nemouchi

## References

Thierry Jéron, Margus Veanes and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021).

*Dagstuhl Reports*3(1):1–29, 2013.

[ BibTeX ]Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel. Isabelle/Circus.

*Archive of Formal Proofs*, 2012. \urlhttp://afp.sourceforge.net/entries/Circus.shtml, Formal proof development.

[ BibTeX ]

## Activities in this research area in more detail:

The rest of this page contains outlines of activities of the group ForTesSE. So far, we have in particular:

- Modeling Sequence and Unit-Testing in HOL.
- Modeling Systems in UML/OCL for Unit Testing
- Testing based on Process Algebra Specifications
- Modeling Security Policies
- Modeling Operating Systems and Embedded Systems
- Extending the Isabelle Platform (Plug-In Mechanisms, Pervasive Parallelism)