Efficient Reasoning Techniques for Large Scale Feature Models

by Mendonca, Marcilio

Abstract (Summary)
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.

Bibliographical Information:


School:University of Waterloo

School Location:Canada - Ontario

Source Type:Master's Thesis

Keywords:software product lines feature models binary decision diagrams sat solvers model reasoning computer science


Date of Publication:01/01/2009

© 2009 All Rights Reserved.