In the work presented in this thesis, supported by the ANR TASCCC project, we propose a test generation technique using behavioral models in UML/OCL and temporal properties. To this end, we describe a temporal property langage based from the property patterns introduced by Dwyer et al. in [DAC99]. A property is a combination of a scope, representing the considered execution pathes in the system, and a pattern, a property that has to be satisfied inside the scope. We then give to each scope and pattern a specific automata-based semantics, called substitution automata. By combining a scope automaton with a pattern automaton, we obtain an automaton representing the semantics of the property. Next, we described nominal coverage criteria, based from classical coverage criteria over automata, specific to our property automata. These criteria focus on informations from the originating property, such as the property events, its scope and its pattern. We complemented this approach with another criterion that, by mutations over events held by certains transitions, aims at activating potentially faulty executions of the system by provoking forbidden events in the automata. We then described for each criterion an algorithm that aims at extracting pathes in the automata with respect to the considered criterion. These pathes are then translated to scenarios in an ad hoc langage that we defined. Finally, an unfolding process over these scenarios, with the help of driving commands embedded in the scenarios, allows the generation of abstract test cases. Finally, our approach has been validated on the study case presented in this document and on GlobalPlatform, an industrial-sized study case in the TASCCC project.
