Constructing Constraint-Preserving Interaction Schemes in Adhesive Categories

摘要

When using graph transformations to formalize model transformations, it is often desirable to design transformations that preserve consistency with respect to a given set of (model) integrity constraints. The standard approach is to equip transformations with suitable application conditions such that the introduction of constraint violations is prevented. This may lead to rules that are applicable seldom or even inapplicable at all, though. To supplement this approach, we present a new and systematic procedure to develop correct-by-construction transformations with respect to a special kind of constraints. Instead of controlling the applicability of a rule we complement its action in such a way that a given constraint holds after application: For every way in which the rule could introduce a violation of the constraint, we derive a supplementary action for the rule that remedies that violation. We formalize this construction in the setting of adhesive categories for monotonic rules and positive atomic constraints and present sufficient conditions for its correctness.