Algebraic Laws for Feature Models

Software Product Lines (SPL) may be adopted by either bootstrapping existing software products into a SPL, or extending an existing SPL to encompass an additional software product. Program refactorings are usually applied for carrying out those tasks. The notion of SPL refactoring is an extension of the traditional definition of refactoring; it involves not only program refactorings, but also Feature Model (FM) refactorings, in order to improve configurability. However, FM refactorings are hard to define, due to the incompleteness of the refactoring catalogs developed as of today. In this paper, we propose a complete, sound catalog of algebraic laws, making up special FM refactorings that preserve configurability. This catalog is also defined as minimal, as one law cannot be derived from another one in the same catalog. In addition, a theory for FMs is presented, in the context of a theorem prover.