Tobias-Z: An executable formal specification of a test generator

Tobias is a combinatorial testing tool that was used succesfully on several case studies. Currently, the evolution of the tool goes through a significant redevelopment effort. A first step is the production of an executable specification of the Tobias Test Generator. The goal of this specification effort is to provide a synthetic and precise description of Tobias to the developers of the new tool. The specification is expressed in the Z language, supported by the Jaza animator. The executable character of the specification is exploited (1) to assess non-regression of the specification with respect to the existing tool, and (2) to explore new functionalities for the tool