A theory for feature models in alloy

Feature models are used to state the instances of a soft-ware product-line. However, there is a limited tool support for automatically checking properties of feature models. In this paper, we propose a theory of feature models in Alloy. This theory can be used to check a number of properties in the Alloy Analyzer. For instance, we show how to check whether general feature model transformations preserve the well-formedness rules of feature models. This theory is com-pared with an alternative theory in Alloy for checking fea-ture model refactorings