Tobias is a test generation tool based on the combinatorial unfolding of a test schema. This unfolding results into a large set of test cases that need to be associated to an automated oracle to produce adequate verdicts. Such automated oracles are typically based on executable specifications such as JML for Java. The design of the tool makes it easy to adapt it to various targets and associated test oracle technologies.

Tobias is an ASE tool (Automated Software Engineering) and as such is subject to two classical ASE challenges: (a) algorithmic problems, here combinatorial explosion, (b) the knowledge bottleneck, ie how to capture useful input information for the tool from its users. The tool has been used on several case studies which show how Tobias addresses these ASE challenges. The knowledge bottleneck is solved by providing the user with a simple input language, at the cost of potentially generating some useless test cases. Combinatorial explosion is addressed by both human intervention and automated techniques. The case studies have also shown how the tool improves the productivity of the test engineer, and helps discovering errors in the programs.

Recently, the tool was used as a complement to proof techniques. Starting from a Java application specified in JML, an automated proof activity can be first carried out to establish the conformance of the program to its specification. When automatic proof fails, Tobias tests are selected which target the area of the application concerned with the failing proof obligation. Mutation techniques are then used to evaluate the quality of the testing campaign and decide whether it is worth to proceed with an interactive proof process.

Bio:
Yves Ledru is Professor at the University Joseph Fourier (Grenoble, France). He received an Engineering degree from the Faculty Polytechnique de Mons (Belgium) and a Ph.D. degree from the University Catholique de Louvain. Since 1993, he is a member of the LSR/IMAG laboratory. His research is in the field of Software Engineering and Formal Methods. Current research activities include the combinatorial generation of test cases in the context of model-based specifications, and integration of formal and graphical specification formalisms. He is the chair of the Steering Committee of the International Conference on Automated Software Engineering and has served on the Program Committees of several international conferences in Software Engineering and Formal Methods.