  We present in this paper a model-based testing approach aiming at generating
test cases from a UML/OCL model and a given test property. The property is
expressed using a dedicated formalism based on patterns, and automatically
translated into an automaton. We propose new automata coverage criteria that
are tailored to the property automata we consider. These criteria are based on
the coverage of a relevant subset of the transitions related to the original
property, aiming at producing test cases that illustrate the dynamics of the
system described in the property. In addition, we propose to produce test cases
that can ensure the robustness of the system w.r.t. the property, by mutating
the property automaton, in order to try to provoke events that would be
forbidden by the property. This approach has been implemented into a large tool
set and it has been experimented on realistic case studies, in the context of
industrial research projects.
