Aujourd'hui, le domaine de la modélisation et de la validation formelle de logiciels est un enjeu majeur du génie logiciel. Plus spécifiquement, les architectures logicielles des systèmes embarqués doivent être conçues pour assurer des fonctions critiques soumises à des contraintes très fortes en termes de fiabilité et de performances temps réel. Malgré les progrès techniques, la grande taille de ces systèmes facilite l'introduction d'une plus grande gamme d'erreurs. Alors, les méthodes formelles ont contribué les solutions rigoureuses et puissantes à produire des systèmes non défaillants. Dans ce domaine, les techniques de model-checking ont été fortement popularisées grâce à leur faculté d'exécuter automatiquement des preuves de propriétés sur des modèles logiciels. Alors, il faut pouvoir gérer à partir des modèles UML des codes formels pour différents outils model-checkers selon le type d'analyse que l'on veut mener. Dans ce travail, le langage pivot Fiacre est choisi comme le langage formel intermédiaire de transformation de modèles UML. Ce langage est exploitable par des outils model-checkers OBP Explorer et TINA. On a défini des règles de transformation qui permet de transformer le modèle structurel et fonctionnel UML vers programmes Fiacre. Les diagrammes de classes sont traduits pour construire la structure du système et les diagrammes d'états sont traduits pour construire la dynamique du système. Les diagrammes d'objets sont traduits pour construire la configuration initiale du système. Une classe active UML et sa machine d'état sont traduites par un processus Fiacre et son comportement et une classe inactive UML est traduite par un type de record en Fiacre. Afin d'établir des règles de transformation, on a proposé deux approches qui permettent de les valider : 1. Montrer la préservation des propriétés lors des transformations en Fiacre. 2. Montrer l'équivalence des sémantiques d'exécution entre le monde UML et le monde Fiacre.