Planning Abstract Consistency Repairs Between Heterogeneous Models

Asserting, maintaining, and repairing consistency between heterogeneous models is a central challenge in model-driven development. Consistency is often defined at the semantic level, but consistency repair techniques typically operate at the syntactic level via language-specific model transformations. This mismatch motivates a shift of perspective: consistency repair should be planned at the semantic level. Building on the notion of observables as a shared semantic space, we introduce contracts as abstractions of model transformations, and we prove key correctness properties. Contracts then capture effects on observable states instead of syntactic changes. We obtain a uniform formalism in which consistency repair can be formulated as a planning problem over set-valued observable states under the goal of restoring consistency. We provide a concrete representation of observable states using abstract domains and cover a representation of contracts via pre- and post-conditions expressed in a logic suitable for automated analysis. This representation allows the use of off-the-shelf formal-methods techniques, such as SAT/SMT-based bounded search and symbolic model checking, to synthesize repair plans. We demonstrate the feasibility of the approach by implementing a prototype in nuXmv, showing how repair plans can be automatically synthesized for a representative heterogeneous modeling scenario.

13th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2026