Automated Verification by Declarative Description of Graph Rewriting-Based Model Transformations

Abstract

Usually, verification of graph rewriting-based model transformations is performed manually, however, the industrial applications require automated methods. In several cases, transformation developers are interested in the offline analysis, when only the definition of the transformation and the specification of the modeling languages are taken into account. Hence, the analysis must be performed only once, and the results are independent from the concrete input models. For this purpose, transformations should be specified in a formalism that can be automatically analyzed. Based on our previous work that presented the mathematical background, this paper provides a platform-independent, declarative formalism for the specification of graph rewriting-based model transformations, and demonstrates its applicability on a case study of refactoring mobile-based social network models. Our results prove that several functional properties of the model transformations can be automatically verified, moreover, the capabilities of our methods can be extended in the future.