Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions

Triple graph grammars are a successful approach to describe exogenous model transformations, i.e. transformations between models conforming to different meta-models. Source and target models are related by some connection part, triple rules describe the simultaneous construction of these parts, and forward and backward rules can be derived modeling the forward and backward model transformations. As shown already for the specification of visual models by typed attributed graph transformation, the expressiveness of the approach can be enhanced significantly by using application conditions, which are known to be equivalent to first order logic on graphs. In this paper, we extend triple rules with a specific form of application conditions, which enhance the expressiveness of formal specifications for model transformations. We show how to extend results concerning information preservation, termination, correctness, and completeness of model transformations to the case with application conditions. We illustrate our approach and results with a model transformation from statecharts to Petri nets.