Toward Automated Verification of Model Transformations: A Case Study of Analysis of Refactoring Business Process Models

Verification of the transformations is a fundamental issue for applying them in real world solutions. We have previously proposed a formalization to declaratively describe model transformations and proposed an approach for the verification. Our approach consists of a reasoning system that works on the formal transformation description and deduction rules for the system. The reasoning system can automatically generate the proof of some properties. In this paper, we present a case study, to demonstrate our approach of automated verification of model transformations in a multi-paradigm environment