Analysis of Feature Models Using Alloy: A Survey

TL;DR

This survey compares various Alloy-based strategies for analyzing feature models in software product lines, highlighting their relative strengths and weaknesses to guide better encoding choices.

Contribution

It is the first comprehensive comparison of Alloy encoding strategies for feature model analysis, providing best practices and evaluation criteria.

Findings

Different encoding strategies vary in expressivity and efficiency.

The survey identifies the most suitable Alloy approaches for specific analysis needs.

Provides a framework for automated extraction and analysis of feature models from natural language requirements.

Abstract

Feature Models (FMs) are a mechanism to model variability among a family of closely related software products, i.e. a software product line (SPL). Analysis of FMs using formal methods can reveal defects in the specification such as inconsistencies that cause the product line to have no valid products. A popular framework used in research for FM analysis is Alloy, a light-weight formal modeling notation equipped with an efficient model finder. Several works in the literature have proposed different strategies to encode and analyze FMs using Alloy. However, there is little discussion on the relative merits of each proposal, making it difficult to select the most suitable encoding for a specific analysis need. In this paper, we describe and compare those strategies according to various criteria such as the expressivity of the FM notation or the efficiency of the analysis. This survey is the first comparative study of research targeted towards using Alloy for FM analysis. This review aims to identify all the best practices on the use of Alloy, as a part of a framework for the automated extraction and analysis of rich FMs from natural language requirement specifications.