Model-driven development enables collaborative design across heterogeneous modelling domains, but it also raises the risk of inconsistent models. We study the problem of extracting minimal submodels that preserve cross-domain consistency. Concretely, given two sets of models related by a consistency specification and a model from the first set, we seek an equiconsistent slice, that is, a submodel that preserves the same consistency relationships with models of the second set. Since the definition of equiconsistency quantifies over the complete second set, a direct computation is infeasible (and undecidable in general). Thus, we formulate slicing as a declarative synthesis problem and solve it using counterexample-guided inductive synthesis (CEGIS). The procedure iteratively proposes candidate slices and refines them using counterexamples (models obtained as violation witnesses if a candidate is not a valid slice). Iterating the CEGIS loop converges to equiconsistent, minimal slices within the bounds used by the model finder. We instantiate the abstract equiconsistency slice problem using attributed typed graphs as models, express consistency relations declaratively, and further realize it using relational logic and SAT-based solving. We then obtain an automated synthesis of equiconsistent slices based only on the consistency relation. We evaluate the method on a synthetic dataset to compare three CEGIS implementations: an explicit loop in Alloy, an explicit loop in Alloy*, and a quantified encoding in Alloy*. We highlight their practical trade-offs.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Slicing Models for Equiconsistency with Alloy

  • Marc Thieme,
  • Shobhit Singh,
  • Terru Stübinger,
  • Romain Pascual,
  • Mattias Ulbrich

摘要

Model-driven development enables collaborative design across heterogeneous modelling domains, but it also raises the risk of inconsistent models. We study the problem of extracting minimal submodels that preserve cross-domain consistency. Concretely, given two sets of models related by a consistency specification and a model from the first set, we seek an equiconsistent slice, that is, a submodel that preserves the same consistency relationships with models of the second set. Since the definition of equiconsistency quantifies over the complete second set, a direct computation is infeasible (and undecidable in general). Thus, we formulate slicing as a declarative synthesis problem and solve it using counterexample-guided inductive synthesis (CEGIS). The procedure iteratively proposes candidate slices and refines them using counterexamples (models obtained as violation witnesses if a candidate is not a valid slice). Iterating the CEGIS loop converges to equiconsistent, minimal slices within the bounds used by the model finder. We instantiate the abstract equiconsistency slice problem using attributed typed graphs as models, express consistency relations declaratively, and further realize it using relational logic and SAT-based solving. We then obtain an automated synthesis of equiconsistent slices based only on the consistency relation. We evaluate the method on a synthetic dataset to compare three CEGIS implementations: an explicit loop in Alloy, an explicit loop in Alloy*, and a quantified encoding in Alloy*. We highlight their practical trade-offs.