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.

翻译：模型变换是模型驱动工程的核心，但由于主流变换语言具有不可判定性，形式化验证十分困难。DSLTrans被设计为图灵不完全的语言以提升可验证性，然而早期基于路径条件枚举的验证仍存在指数级爆炸问题，无法扩展到实际案例。我们提出一种可处理的DSLTrans验证工作流，并形式化了其完备性条件。该方法融合三项贡献：(i) 截断定理证明，对于精确的DSLTrans片段及存在性/可追溯性正向属性，有界模型检验是完备的，从而将无限搜索转化为有限可计算边界；(ii) 可组合的保真优化（基于类的边界、基于CEGAR的片段验证及轨迹感知的依赖分析），减小SMT编码规模；(iii) 基于Z3的实现，在ATL Zoo及相关基准测试的真实变换上进行评估。针对涵盖编译器降级、模式翻译、行为建模、图映射及压力测试的29个具体变换和899个属性，552个属性被证明，345个产生具体反例（包括有意设置的负面和边界情况），仅有2个因超时未决。对于超出可处理预算的属性，我们引入可处理性驱动的细化（前提特化、后置条件分解及变换插桩），实现高达112倍加速，同时消除虚假反例。该工作流得到Web集成开发环境及用于运行时验证的具体执行引擎的支持。