Acceptance Tests
The purpose of testing is to provide a reasonable assurance of the correction of the developed code. This also means that tests are not about proving the code is correct: all behavior cannot be inspected. The assurance is provided by a coverage criterion.
Several kind of tests can be distinguished because correction can be expressed in relation with different kinds of documents expressing the system behavior at different levels : from the component level (unit tests), design level (integration tests), up to the software reception by the customer (acceptance tests). Those levels are best illustrated by the "V-model" in the following figure.

- The V-Model.
The purpose of the FAUST toolbox is to help achieving high assurance in the Requirements Engineering (RE) process. With respect to testing its area is acceptance testing. The approach is goal-oriented and the acceptance tests cases are thus generated from a goal-model. It has a number of interesting properties:
test generation does not require an operational model: a prescriptive model is enough (ie. a model stating the required properties but now how to achieve them). This allows one to genere high level tests without imposing specific design choices.
the coverage criterion is goal-based: the potential system behaviors stated in the goals have to be covered.
besides the goals, others concepts are also taken into accounts such as the possible refinement pattern (such as case/milestone) and obstacles/conflicts (ie impedimenting the goal realisation and thus revealing limit conditions)
In this introductory article we will just highlight how the test generator works without entering into implementation details which rely on constraint programming. For more information the interested reader is directed to the article "Deriving Acceptance Tests from Goal Requirements".
A Simple Example
As simple example, let’s consider an elementary train boarding system depicted hereafter. The system is composed of a boarding block with a direct access to it and a waiting block in case a train is already on the boarding block.

- Train Example: Domain.
Among the goals, one can distinguish:
progress goals, stating that every incoming train will eventually leave the system unloaded.
safety goals: train crash have to be avoided. In our system we will explicitely choose a block system design with at most one train per block.
In this example, acceptance tests generation is essentially derived from the progress goals so we will only refine them in the following figure:

- Train Example: Goal Model
In the process of the elaboration of that goal model, the following object model stating the vocabulary used in the temporal logic assertion is also produced.

- Train Example: Object Model.
Acceptance Tests Generation
The acceptance tests generation process is composed of two major steps:
acceptance tests classes are elaborated, for now mainly based on the information in the goal refinements. In the above example composed of one "case" refinement and two "milestone" refinement: the case refinement will give rise to two classes of step-by-step temporal behaviors.
best representatives are chosen in those tests classes based on a number of heuristics such as minimal length traces (maximal progress), reaching limit conditions (temporal constraints, untils...). Moreover some well chosen contextual information is also required such as initial/final states, and the number of instances being considered.
Acceptances tests are generated by unfolding temporal formulas which can be translated into a constraint problem for exploring all possible behaviors. Additional constraints are then added for specifying tests classes and the representative selection criterion. The resulting set of constraints is fed into a constraint solver that yields a concrete test trace.
The resulting trace can be depicted as a scenario between the system under test and its operational environment. As exemple the following figure shows an interesting limit test where two trains are introduced into the system: the first heading directly to the unload block and the second going through the waiting block until the unload block becomes free.

- Train Example: Generated Test.
