Presence Condition Reasoning with Feature Model Interfaces : Master’s Thesis

Family-based static analysis techniques allow to efficiently analyze the exponential variant space of a software product line (SPL). Rather than analyzing each variant completely on its own, a family-based analysis processes information shared among multiple variants only once. The analysis delegates parts of the exponential complexity to reasoning about boolean presence conditions, which control the inclusion or exclusion of code fragments in a particular variant. The feature model of the SPL, which determines the set of valid variants, must be included in the reasoning process to obtain correct results. However, typically not all parts of a feature model arerelevant for a particular condition. In this work, we propose a method to accelerate presence condition reasoning by decreasing the size of the model used for reasoning. In particular, we use the concept of feature model interfaces to decompose a feature diagram according to its hierarchical structure, and obtain an abstraction that can be selectively refined on the fly for a given condition. We formalize our approach in terms of propositional feature diagram semantics and prove its correctness. In our evaluation, we demonstrate that our approach accelerates reasoning by up to 24 percent.