Basic ExampleUser ManualIntroductionContentsIndex


Tool principles


Most existing test generation tools perform their analysis by enumerating the specification state space. This leads to two problems:

To avoid these problems we introduce symbolic generation techniques.


STG (Symbolic Test Generator) generates conformance tests, based on this framework:

Three possible verdicts:

Tool Architecture

Here is the architecture of STG:


STG is implemented in Ocaml. The two parsers are generated with Ocamllex and Ocamlyacc. We use NBAC to simplify test cases produced by STG, and LUCKY to instantiate symbolic values during test case execution. The tool  Dotty is used to display automata.

Conformance Testing and IOSTS Model

Conformance testing

Conformance testing is a methodology for validating reactive systems. It consists in testing a conformance relation between a specification of the system, which is a physical process that can only be controlled and observed at its interfaces. This is done by running test cases on the implementation and obtaining verdicts about the conformance. In general three kind of verdicts are distinguished. Informally, Fail means that non-conformance was detected, Pass means that the implementation behaved in conformance with specification and the goal of the test experiment (described by a test purpose) has been reached, and Inconclusive means that the implementation behaved correctly but, due to the lack of control on the implementation, it did not allow to reach the expected goal. We model specifications, implementations, test purposes and test cases as IOSTS, with some restrictions on each category.


(Input/Output Symbolic Transition Systems) are a model for reactive programs with symbolic processing of variables, parameters, and inter-process value passing. The syntax and semantics are formally defined in [2]. We use IOSTS for describing specifications, test purposes, and test cases, and assume nothing about black-box implementation other than that it is interface-compatible with the specification. Furthermore, we restrict our attention here to specifications and implementations that are command-response, meaning that an input, or sequence of inputs, may only be followed by at most one output(i.e., a command is followed by at most one response). Here is an example an iosts specification

Test Generation


Symbolic test generation consists of computing, from a specification and a test purpose, a test case that covers all the behaviors of the intersection of these two elements. Then, the test case is translated into executable code to be run on a black-box implementation. Test generation consist on the following steps.

Correctness of test case.

In [2] we prove that the generated test case have, by construction, a set of correctness properties, meaning essentially that they do not produce false "`Pass", "Fail" and "Inconclusive" verdicts. Furthermore, every test case generated from a given specification and test purpose has a relative completeness property, meaning that a "`Fail" verdict will be produced in every circumstance where the implementation exhibits a non conformance with the specification in a behavior targeted by the test purpose.

F Ployette, F-X Ponscarme, March 21, 2007

Basic ExampleUser ManualIntroductionContentsIndex