Generating Preconditions from Graph Constraints by Higher Order Graph Transformation

Abstract: Techniques for the verification of structural invariants in graph transfor-mation systems typically rely on the derivation of negative application conditions that are attached to graph transformation rules in order to avoid the runtime occur-rence of forbidden structural patterns in the system model. In this paper, we propose a practical approach for this derivation process, which produces the required neg-ative application conditions by applying higher order graph transformation on the rule specifications themselves. Additionally, we integrate filtering criteria into these higher order constructs to avoid, already at an early stage, the unnecessary construc-tion of invalid and redundant negative application conditions