Computing Attribute Ranges for Partial Configurations with JavaSMT : Bachelor's Thesis
Software product lines are able to describe multiple products sharing a common base of features and are commonly described as feature models. For complex software product lines, automatic analyses are required to ensure validity and to improve the interactive conﬁguration process. Modern SAT solvers are vital components for the validation process of feature models. The increasing variability of software product lines implies the need to use more expressive solvers like SMT solvers. To assist the development of feature modeling tools, we compare SAT and SMT solvers for the automated analysis of feature models. During this thesis, we create an abstract data type to formally deﬁne analyses for feature model defects and their explanations. The result shows that SAT solvers are more eﬃcient at detecting the defects, while SMT solvers can ﬁnd explanations for them multiple times faster. Feature models can be further expanded by attaching attributes to features. Such attributes may contain a numerical value. Additionally, one attribute can be deﬁned for multiple features. In this thesis, we aim to support the interactive conﬁguration process, by providing the range of the sum of values for an attribute. Such ranges depend on the remaining choices in a conﬁguration of the product line. We provide an exact computation using SMT and an approximation using a heuristic. The evaluation results show that an SMT solver is not suitable for supporting interactive conﬁguration. However, the approximated ranges of the provided heuristic were very close to the exact ones.