Constructing optimized constraint-preserving application conditions for model transformation rules

摘要

There is an increasing need for model transformations ensuring valid result models w.r.t. a given constraint. In model refactoring, for example, each performed refactoring should yield a valid model again. Given a constraint, if a model transformation rule always produces valid output, it is calledconstraint-guaranteeing; if only when applied to an already valid model, it is calledconstraint-preserving. In the literature, there is a formal construction for model transformation systems making them constraint-guaranteeing. This is ensured by adding application conditions to their transformation rules. These conditions can become quite large, though. As there are interesting application cases where transformations just need to be constraint-preserving (such as model refactoring), the construction of application conditions was also adapted to this case. Although logically weaker, the straightforward construction can lead to even larger application conditions. In this work, we develop simplifications of constraint-guaranteeing conditions by omitting certain parts of these conditions, namely of parts that check for antecedent validity. We prove that the resulting application conditions are constraint-preserving and characterize their logical strength. Our theory is developed forM-adhesive categories which encompass various graph-like model structures. In addition, the computation of constraint-guaranteeing application conditions and their simplifications was implemented in the Eclipse plug-in OCL2AC. Evaluations show that the complexity of the constructed simplified conditions is reduced by factor 7 on average. Moreover, this optimization yields a speedup of rule application by approximately 2.5 times.