Proving Model Transformations

Within the MDA context, model transformations (MT) play an important role as they ensure consistency and significant time savings. Several MT frameworks have been deployed and successfully used in practice. Like for any software, the development of MT programs is error prone. However there is limited support for verification and validation in current MDA technologies. This paper presents an approach to prove model transformations. Model transformations are firstly formalized in B. Then the B provers will be used to analyze and prove the correctness of transformation rules w.r.t. met models and transformation invariants. We also analyze and prove the consistency of transformation rules w.r.t. each other.