Towards Formal Analysis of Multi-paradigm Model Transformations

The Multi-Paradigm Modeling (MPM) approach of model-based development emphasizes the specification of a system by multiple models. We use transformations to automatically transform, integrate and synchronize models. Verification and validation of model transformations are fundamental issues: we need to express what a valid model is and how a valid model transformation may transform the models; otherwise, we have to analyze each transformed model individually, which makes it difficult to automate the process of using models. We have formally analyzed various model transformations in several case studies and industrial projects. From this experience, we have distilled the frequently recurring techniques and solutions, referred to as Model Transformation Analysis (MTA) methods. These instances, similarly to design patterns in object-oriented programming, define special constructions as solutions for recurring problems that arise when one implements a model transformation. Moreover, MTA methods contain special techniques and language features that should be taken into account when one designs a model transformation framework or a model transformation language. We hope that MTA methods may be the basis of automated formal analysis techniques of model transformations. This paper contributes the concept and instances of MTA methods and provides a case study based on an industrial project of mobile application development. With this real-world example, we want to demonstrate the role and use of MTA methods. The case study is implemented in Visual Modeling and Transformation System (VMTS), which is a tool that realizes the MPM concept to provide a model and model transformation-based environment for software development.