UML est l'un des langages les plus rp̌andus pour la conception des applications informatiques. Il ťant un langage semi-formel, le principal reproche d'UML est l'absence de bases formelles permettant l'application des techniques de vřifications formelles. Il ne dispose d'aucuns outils pour la vřification et la preuve des propriťš de ces modl̈es.
L'approche la plus largement adoptě est la transformation d'un modl̈e UML vers une spčification formelle, en utilisant des mťhodes formelles comme FoCaLiZe. Cette approche rentre dans le cadre d'ingňierie de modl̈es (MDE, "Model Driven Engineering"), qui vise la production de softwares par raffinements automatiques de modl̈es, depuis les spčifications abstraites jusqu'aux implm̌entations concrẗes.
FoCaLiZe est un environnement complet pour exprimer tous ces aspects du dv̌eloppement logiciel.
Dans cette mm̌oire, nous proposons une approche MDE pour la transformation automatique des diagrammes d'ťats-transitions UML en spčifications FoCaLiZe, puis une implm̌entation des rg̈les de transformation en utilisant le langage XSLT qui nous permet de gňřer une spčification FoCaLiZe p̉artir d'un document XMI (XML Meta data Interchange).