Analysis and evaluation of conformance preserving graph transformation rules

Abstract

Model transformation is a formal approach for modelling the behavior of software systems. Over the past few years, graph based modeling of software systems has gained significant attention as there are numerous techniques available to formally specify constraints and the dynamics of systems. Graph transformation rules are used to model the behavior of software systems which is the core element in model driven software engineering. However, in general, the application of graph transformation rules cannot guarantee the correctness of model transformations. In this paper, we propose to use a graph transformation technique that guarantees the correctness of transformations by checking required and forbidden graph patterns. The proposed technique is based on the application of conformance preserving transformation rules which guarantee that produced output models conform to their underlying metamodel. To determine if a rule is conformance preserving we present a new algorithm for checking conformance preserving rules with respect to a set of graph constraints. We also present a formal proof of the soundness of the algorithm. We apply our technique to homogeneous model transformations where input and output models must conform to the same meta-model. The algorithm relies on locality of a constrained graph to reduce the computational cost.