Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces a tractable verification workflow for DSLTrans, a domain-specific language for model transformations, by proving a Cutoff Theorem that enables complete bounded model checking for a fragment of DSLTrans. They combine this theorem with soundness-preserving optimizations like per-class bounds and CEGAR-based fragment verification to reduce SMT encoding size, and implement their approach using Z3. Experiments on a suite of realistic transformations demonstrate the ability to prove or find counterexamples for a large number of properties, with tractability-driven refinement further improving performance.
Bounded model checking, previously impractical for verifying model transformations, can now be made tractable and complete for a useful fragment of DSLTrans via a novel Cutoff Theorem.
Model transformations are central to MDE, but formal verification is difficult because mainstream transformation languages are undecidable. DSLTrans was designed to be Turing-incomplete to improve verifiability, yet earlier verification based on path-condition enumeration still suffered exponential blow-up and did not scale to realistic cases. We present a tractable verification workflow for DSLTrans and formalize when it is complete. The method combines three contributions: (i) a Cutoff Theorem proving that bounded model checking is complete for a precise DSLTrans fragment and positive existence/traceability properties, turning an infinite search into a finite computable bound; (ii) composable, soundness-preserving optimizations (per-class bounds, CEGAR-based fragment verification, and trace-aware dependency analysis) that reduce SMT encoding size; and (iii) a Z3-based implementation evaluated on realistic transformations from the ATL Zoo and related benchmarks. On 29 concrete transformations and 899 properties spanning compiler lowering, schema translation, behavioral modeling, graph mapping, and stress tests, 552 properties are proved, 345 produce concrete counterexamples (including intentional negative and boundary cases), and only 2 remain undecided within timeout. For properties beyond the tractability budget, we introduce tractability-driven refinement (precondition specialization, postcondition decomposition, and transformation instrumentation), achieving up to 112x speedup while eliminating spurious counterexamples. The workflow is supported by a web IDE and a concrete execution engine for runtime validation.