UML-based methodologies take more and more space in the software development domain. In addition, the need to validate applications as early as possible in the development cycle is now mandatory to satisfy cost and time-to-market constraints. In this context, this paper describes, first, how to bridge the gap between semiformal UML models and a formal technology ensuring test case generation. Second, the formal tool used to automatically generate test sequences, named AGATHA, is described in minute detail. Finally, this approach is illustrated throughout by a toy example of an elevator system.