通过约束提升对模型产品线的通用分析

工程化一个产品线不仅仅是描述一个产品线：为保证正确，每一个可生成的变体都必须满足某些约束。为确保所有这些变体均正确（例如良类型），仅有两种途径：要么逐个检查感兴趣的变体，要么针对每种约束设计复杂的产品线分析算法。本文探讨该问题的一种泛化：我们提出一种机制，可检查某一约束是否对可能生成的所有变体同时成立。本文的主要贡献是一个函数，它接受应为所有变体满足的约束，并从中生成（“提升”出）针对产品线的约束。这些被提升的约束可直接在模型产品线上检验，从而对所有变体同时验证。该提升以非常通用的方式表述，允许以模块化方式利用如 SMT 求解或定理证明等通用算法。我们展示了如何通过自动翻译模型产品线与约束，利用 SMT 求解验证被提升的约束。该方法的适用性通过一个工业案例研究得以展示，其中我们将提升应用于一个面向制造规划的领域特定建模语言。最后，运行时分析通过对来自 BMW Group 与 Miele 的生产规划数据所构建的不同模型产品线进行分析，显示了可扩展性。