Registered user since Fri 6 May 2022
Contributions
Feature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. With this artifact, we contribute a fully automated software and a replicatable dataset for comparing three CNF transformations (i.e., distributive, Tseitin, and Plaisted-Greenbaum) on a corpus of 22 real-world feature models.
Research Papers
Thu 13 Oct 2022 16:10 - 16:30 at Banquet B - Technical Session 32 - Formal Methods and Models II Chair(s): Khouloud GaaloulFeature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. In this paper, we compare three transformations (i.e., distributive, Tseitin, and Plaisted-Greenbaum) for bringing feature-model formulas into CNF. We analyze which transformation can be used to correctly perform feature-model analyses and evaluate three CNF transformation tools (i.e., FeatureIDE, KConfigReader, and KClause) on a corpus of 22 real-world feature models. Our empirical evaluation illustrates that some CNF transformations do not scale to complex feature models or even lead to wrong results for certain analyses. Further, the choice of the CNF transformation can substantially influence the performance of subsequent analyses.
