Generic Analysis of Model Product Lines via Constraint Lifting
This addresses the challenge of ensuring correctness for all variants in product-line engineering, particularly in industrial settings like manufacturing planning, though it appears incremental as it builds on existing verification methods.
The paper tackles the problem of verifying constraints for all variants in model product lines by proposing a constraint lifting mechanism that generates constraints for the product-line, enabling simultaneous verification for all variants using generic algorithms like SMT solving, with applicability demonstrated in an industrial case study involving manufacturing planning data from BMW Group and Miele.
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.