Analysis of Feature Models Using Alloy: A Survey

Anjali Sree-Kumar
(Universitat Oberta de Catalunya)
Elena Planas
(Universitat Oberta de Catalunya)
Robert Clarisó
(Universitat Oberta de Catalunya)

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.

In Julia Rubin and Thomas Thüm: Proceedings 7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE 2016), Eindhoven, The Netherlands, April 3, 2016, Electronic Proceedings in Theoretical Computer Science 206, pp. 46–60.
Published: 28th March 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: