Analyzing DOPLER Decision Models with SMT

In software product line engineering, decision modeling is one of the most common approaches to variability modeling. Decision models are particularly suitable to guide users through products and available customization options, which often represent huge configuration spaces and would hence benefit from automated analysis. However, only very few SAT- and SMT-based analysis techniques have been implemented for decision models. In this paper, we propose a novel encoding for decision-modeling concepts in SMT. We implemented our SMT encoding within a DOPLER decision meta-model re-implementation and assessed feasibility and applicability using publicly available models. Our results show that our encoding facilitates unsatisfiability analysis and anomaly detection in DOPLER decision models. With this work, we improve the configuration support of decision modeling with SMT-based analysis.