Abstract—We present in this paper a technique based on symbolic animation of models that aims at producing modelbased tests. In order to guide the animation of the model, we rely on the use of a deterministic finite automaton (DFA) of the model that is built using a well-known learning machine algorithm from Angluin, considering a complex model as a black-box component that can be animated. Since the DFA obtained in this way may be an over-approximation and, thus, admit traces that were not admitted on the original model, this abstraction is refined using counter-examples made of unfeasible traces. The computation of counter-examples is perfomed using a systematic coverage of the DFA states and transitions, producing test sequences that are replayed on the model, providing either test cases for offline testing, or counterexamples that aim at refining the abstraction.