Model Driven Architecture (MDA) design approach proposes to separate design into two stages: implementation independent stage then an implementation-dependent one. This improves the reusability, the reliability, the standability, the maintainability, etc.
Here we show how MDA can be augmented using a formal refinement approach: B method. Doing so enables to gradually refine the development from the abstract specification to the executing implementation through many controled steps. Each refinement step is mathematicaly represented and is proven to be correct, by conceconce then the implementention is proven to satisfy the specification; furthermore this approach permits to prove the coherence between components in low levels even if they are branched in different technologies during the development.