The goal of this work package is to define techniques for harnessing the configuration complexity for co-dependent, co-existing configurations in order to reduce the testing effort needed to detect and validate the properties of the whole system that cannot be ensured at the model level. To achieve this goal WP4 is to develop a reasoning framework for validation for co-dependent, co-existing configurations. This framework shall serve two purposes:

1. it will allow to check whether a specific configuration is fit for the intended purpose, and

2. it will allow to find and rate configurations having predefined properties.

Since the number of variants combinations (and thus application behaviours) grows exponentially with the number of variation points, it is not materially possible to validate each potential variant of the application separately. Inspired by the notion of Design-by-Contract, we define a model for adaptation aspects in order to enhance them with assume/guarantee clauses. The adaptation aspects represent the configuration variability dimensions (variation points) identified in WP1 implemented using the techniques being developed in WP2 and WP3. The compatibility between clauses can then be checked statically  while the conformance of an adaptation aspect to its assume/guarantee clauses will be tested based on standard unit testing principles, adapted with test criteria based on the analysis of adaptation models.

The former work packages permit to check whether a given configuration fits into the variability model. To facilitate exploration of the variability space from a different perspective, WP4 will also research an approach for checking existence and deriving of candidate configurations with searched-for properties from the same variability model.

This conceptual framework is in WP5 implemented and integrated within the Diva Tool suite.

FaMa Tool Suite is considered to serve as the base framework for the adaptation reasoning & validation engine of DiVA work package 4.

FaMa Tool Suite is based on several tools. One of them is FaMa-FW that is a framework for automated analysis of feature models, integrating some of the most commonly used logic representations and solvers proposed in the literature (BDD, SAT and CSP solvers are implemented). FaMa is the first tool integrating different solvers for the automated analysis of feature models. FaMa is published under the GNU Lesser General Public License.