Engineering a product-line is more than just describing a product-line: to be correct, every variant that can be generated must satisfy some constraints. To ensure that all such variants will be correct (e.g. well-typed) there are only two ways: either to check the variants of interest individually or to come up with a complex product-line analysis algorithm, specific to every constraint. In this paper, we address a generalization of this problem: we propose a mechanism that allows to check whether a constraint holds simultaneously for all variants which might be generated. The main contribution of this paper is a function that assumes constraints that shall be fulfilled by all variants and generates ("lifts") out of them constraints for the product-line. These lifted constraints can then be checked directly on a model product-line, thus simultaneously be verified for all variants. The lifting is formulated in a very general manner, which allows to make use of generic algorithms like SMT solving or theorem proving in a modular way. We show how to verify lifted constraints using SMT solving by automatically translating model product-lines and constraints. The applicability of the approach is demonstrated with an industrial case study, in which we apply our lifting to a domain specific modelling language for manufacturing planning. Finally, a runtime analysis shows scalability by analyzing different model product-lines with production planning data from the BMW Group and Miele.

翻译：工程化一个产品线不仅仅是描述一个产品线：为了确保正确性，每个可生成的变体都必须满足某些约束。要保证所有此类变体都正确（例如类型良好），只有两种方法：要么逐个检查感兴趣的变体，要么为每种约束设计复杂且特定的产品线分析算法。本文针对该问题的泛化形式展开研究：我们提出一种机制，允许同时检查某个约束是否对所有可能生成的变体都成立。本文的主要贡献在于提出一个函数，该函数接收所有变体应满足的约束，并从中生成（“提升”）针对产品线的约束。这些提升后的约束可直接在模型产品线上进行检验，从而同时验证所有变体。提升过程以高度通用的方式表述，使得能够以模块化方式利用SMT求解或定理证明等通用算法。我们展示了如何通过自动翻译模型产品线与约束，使用SMT求解验证提升后的约束。该方法的适用性通过工业案例研究得到验证，其中我们将提升技术应用于制造规划领域的特定领域建模语言。最后，通过使用宝马集团和美诺公司的生产规划数据对不同模型产品线进行分析，运行时分析证明了该方法的可扩展性。