| dc.description.abstract | In Software Product Lines (SPLs), a feature model can be used to represent the
similarities and differences within a family of software systems. This allows
describing the systems derived from the product line as a unique combination of
the features in the model. What makes feature models particularly appealing is
the fact that the constraints in the model prevent incompatible features from
being part of the same product.
Despite the benefits of feature models, constructing and maintaining these models
can be a laborious task especially in product lines with a large number of
features and constraints. As a result, the study of automated techniques to
reason on feature models has become an important research topic in the SPL
community in recent years. Two techniques, in particular, have significant
appeal for researchers: SAT solvers and Binary Decision Diagrams (BDDs). Each
technique has been applied successfully for over four decades now to tackle
many practical combinatorial problems in various domains. Currently, several
approaches have proposed the compilation of feature models to specific logic
representations to enable the use of SAT solvers and BDDs.
In this thesis, we argue that several critical issues related to the use of SAT
solvers and BDDs have been consistently neglected. For instance, satisfiability
is a well-known NP-complete problem which means that, in theory, a SAT solver
might be unable to check the satisfiability of a feature model in a feasible
amount of time. Similarly, it is widely known that the size of BDDs can become
intractable for large models. At the same time, we currently do not know
precisely whether these are real issues when feature models, especially large
ones, are compiled to SAT and BDD representations.
Therefore, in our research we provide a significant step forward in the
state-of-the-art by examining deeply many relevant properties of the feature
modeling domain and the mechanics of SAT solvers and BDDs and the sensitive
issues related to these techniques when applied in that domain. Specifically, we
provide more accurate explanations for the space and/or time (in)tractability of
these techniques in the feature modeling domain, and enhance the algorithmic
performance of these techniques for reasoning on feature models. The
contributions of our work include the proposal of novel heuristics to reduce the
size of BDDs compiled from feature models, several insights on the construction
of efficient domain-specific reasoning algorithms for feature models, and
empirical studies to evaluate the efficiency of SAT solvers in handling very
large feature models. | en |
