Supporting Multi-level Configuration with Feature-Solution Graphs -- Formal Semantics and Alloy Implementation

In Software Product Lines, several approaches support configuration processes using feature models representing constraints about which features, software elements or assets can be included in a product.
These approaches use a single feature models to display users which features can be included in a product and to validate if a given configuration is valid.
In this paper we propose feature-solution graphs (FSGs) to detect and explain conflicts in multi-staged configuration processes.
In these FSGs, configuration options are arranged into a pair of feature models with relationships between them.
Then, when some options are selected in one of them, an automatic process is able to determine the set of options that can be selected in the other.
Finally, if a combination of features results in that none option can be selected in the latter feature model, an automatic process determine the selected options that cause the problem.

The technical report presents the approach providing a formal semantics for feature models and feature solution graphs, and provides an example and comparison.