Generic Analysis of Model Product Lines via Constraint Lifting

TL;DR

This paper introduces a general method for verifying constraints across all variants of a product-line simultaneously by lifting constraints to a model level, enabling scalable and generic analysis using SMT solving.

Contribution

It proposes a novel constraint lifting mechanism that generalizes product-line analysis, allowing for efficient, model-based verification of all variants at once.

Findings

Successfully applied to industrial manufacturing planning case study.

Demonstrated scalability with production data from BMW and Miele.

Enables generic verification using SMT solvers.

Abstract

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.