Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generic Analysis of Model Product Lines via Constraint Lifting

Andreas Bayha, Vincent Aravantinos

TL;DR

This paper tackles the challenge of ensuring correctness across all variants in a model product-line by introducing a generic constraint lifting mechanism. It formulates a formal core for models, adds variability through feature models and symbolic binding, and defines a lifting operator to transform single-model constraints into product-line wide constraints. An SMT-based implementation demonstrates translating models, variability, and lifted constraints into solvable formulas, validated on a SFIT DSML case study with real industrial data from BMW and Miele. The results show successful detection of introduced failures, alignment with existing domain-specific analyses, and practical scalability, supporting broader adoption of language-independent product-line verification methods.

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.

Generic Analysis of Model Product Lines via Constraint Lifting

TL;DR

This paper tackles the challenge of ensuring correctness across all variants in a model product-line by introducing a generic constraint lifting mechanism. It formulates a formal core for models, adds variability through feature models and symbolic binding, and defines a lifting operator to transform single-model constraints into product-line wide constraints. An SMT-based implementation demonstrates translating models, variability, and lifted constraints into solvable formulas, validated on a SFIT DSML case study with real industrial data from BMW and Miele. The results show successful detection of introduced failures, alignment with existing domain-specific analyses, and practical scalability, supporting broader adoption of language-independent product-line verification methods.

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.

Paper Structure

This paper contains 24 sections, 33 equations, 11 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Running Example
  3. Formal Basis: Definition of Non-Variable (Core) Models
  4. Metamodels
  5. Core Models
  6. Constraints
  7. Conceptual Core: Model Product-Lines and Generic Product-Line Analysis by Constraint Lifting
  8. Variability in Models
  9. Symbolic Binding of Product-line Variability
  10. Lifting Constraints to Symbolic Variant Level
  11. Exemplary Implementation Using SMT Solving
  12. Translation of Models
  13. Translation of Variability
  14. Translation of Constraints and Generation of Counterexamples
  15. Case Study: The SFIT DSML for Manufacturing Planning
  16. ...and 9 more sections

Figures (11)

  • Figure \thelstlisting: Motivation and concept for our lifting approach.
  • Figure \thelstlisting: Overview about the structure of this paper and the dependencies between the chapters.
  • Figure \thelstlisting: Metamodel for our running example: the modeling language $\mu L\xspace$.
  • Figure \thelstlisting: The example model "myProgram1" as an object diagram. The textual representation is given in Figure \ref{['lst:prog1']}.
  • Figure \thelstlisting: A feature model for the product-line of $\mu L\xspace$ programs in Figure \ref{['lst:prog3']}.
  • ...and 6 more figures

Theorems & Definitions (7)

  • definition 1: Instances
  • definition 2: Constraint Language $\mathcal{L}\xspace$
  • definition 3: Presence Condition Function
  • definition 4: Model Product-Line
  • definition 5: Configuration
  • definition 6: Binding Function $\downarrow\xspace$
  • definition 7: Lifting Function $\uparrow\xspace$