Refinement and Consistency in Multiview Models

Model transformations are an integral part of OMG's standard for Model Driven Architecture (MDA). Model transformations should at the best allow for a seamless transition from high-level models to actual implementations. They are therefore required to be behaviour preserving: models (or the final implementation) at lower levels should adhere to the descriptions given in higher level models. Moreover, for complex systems models usually consists of descriptions of different views on the system. Consequently, different kinds of model transformations take place on different views, and together they should guarantee behaviourpreservation. In this paper we discuss the applicability of formal methods to model transformations. Formal methods come with build-in notions of transformations between models, or more precisely, with refinement and subtyping concepts which provide means for comparing models on different levels with respect to their behaviour. Such notions can be applied as correctness criteria for evaluating model transformations. Moreover, refinement and subtyping concepts for different views can be shown to neatly fit together. This is achieved by giving a common semantics to all views which furthermore opens the possibility of checking consistency between them.