Verification of models and model processing programs are inevitable in model-based software development in order to apply them in real-world solutions. Verification of properties of model transformations means to prove that the application of a model transformation generates the expected output models from the input models. Model transformation developers are interested in offline methods for the verification process. Offline analysis means that only the definition of the model transformation and the metmodels of the source and target languages are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. In this paper, we propose a formalization to describe model transformation. A formal description can be automatically generated, and can be extended by the experts. An automated reasoning system may prove some properties of model transformations by deriving new assertions from the original description.
展开▼
