CS (http://www.c-s.fr) is in charge to experiment a model to model transformation, in the OpenEmbeDD (http://openembedd.org/home_html) project (an RNTL project). The objective of this experimentation is to provide an operational model verification chain : starting at user level (SDL profiled UML), using an intermediate (or "pivot") language (FIACRE), and terminating at verification level (TINA or CADP). This experimentation uses (and must provide updates of) TOPCASED tools (TOPCASED, http://www.TOPCASED.org/, is an Aerospace Valley project http://www.aerospace-valley.com/en/). It is fundamental work in the context of this project, because it validates a complete approach for critical application models verification. The aim of our paper is to describe this experimentation. First the state of the art and the key points associated to this kind of approaches is presented. Next a detailed description of the made work (meta models, mappings and tools …) and at last a tutorial with the last critical open points and an action list to reach the final objectives.