FAMA: Tooling a Framework for the Automated Analysis of Feature ModelsDavid Benavides, Sergio Segura, Pablo Trinidad and Antonio Ruiz-Cort´esDepartment of Computer Languages and SystemsUniversity of SevilleAv. de la Reina Mercedes S/N, 41012 Seville, Spaine-mail: {benavides, segura, trinidad, aruiz}@tdg.lsi.us.esAbstractThe automated analysis of feature models is recognizedas one of the key challenges for automated software de-velopment in the context of Software Product Lines (SPL).However, after years of research only a few ad-hoc propos-als have been presented in such area and the tool supportdemanded by the SPL community is still insufficient. In pre-vious work we showed how the selection of a logic repre-sentation and a solver to handle analysis on feature modelscan have a remarkable impact in the performance of theanalysis process. In this paper we present a first imple-mentation of FAMA (FeAture Model Analyser). FAMA is aframework for the automated analysis of feature models in-tegrating some of the most commonly used logic represen-tations and solvers proposed in the literature. To the best ofour knowledge, FAMA is the first tool integrating differentsolvers for the automated analyses of feature models.1. IntroductionFeature Modelling is a common mechanism to managevariability in the context of software product lines (SPL).A Feature Model (FM) represents all possible products inan SPL in terms of features. A feature is an increment inproduct functionality. FMs can be used in different stagesof development such as requirements engineering [14, 15] ,architecture definition or code generation [1, 4].Automated analyses of FMs is recognized in the litera-ture as an important challenge in SPL research [1, 3]. Theautomated analyses of FMs is usually performed in twosteps: i) The FM is translated into a certain logic repre-sentation ii) Off-the-shelf solvers are used to extract infor-mation from the result of the previous translation such asthe number of possible products of the feature model, allthe products following a criteria, finding the minimum costconfiguration, etc [6]. In previous works we introduced howthe use of different solvers [7] and logic representations [8]can have an important effect in the time and memory perfor-mance of the analysis process. We also showed that there isnot an optimum logic representations and solver for all theoperations that can be performed on an FM.Existing tools to analyse FMs depend on concrete solversand their performance could be improved if they used sev-eral solvers. Two options arise to support multiple solvers:i) Extending an existing tool to use several solvers, ii) cre-ate our own multi-solver framework that supports any kindof representation and solver and could interoperate with ex-isting tools. We have chosen the second option because theanalysed tools are either not open–source tools or they arenot prepared to be adapted to support multiple solvers.In this paper we present a first prototype implementa-tion of FAMA. FAMA is an extensible framework for theautomated analysis of feature models. FAMA allows theintegration of different logic representations and solvers inorder to optimize the analysis process. It can be config-ured to select automatically in execution time the most effi-cient of the available solvers according to the operation re-quested by the user. The current implementation of FAMAintegrates three of the most promising logic representationsproposed in the area of the automated analysis of featuremodels: CSP, SAT and BDD, but more solvers can be addedif needed. The implementation is based on an Eclipse plug–in and uses XML to represent FMs so it can interoperatewith other tools that support it.The remainder of the paper is structured as follows: inSection 2 the automated analysis of FMs is outlined anddetails of the performance offered by the solvers used arepresented. Section 3 focuses on the description of the func-tionality and some of the most relevant design and imple-mentations details of the framework. A brief overview ofsome related tools is introduced in Section 4. Finally wesummarize our conclusions and describe our future work inSection 5.2. Automated Analysis of Feature ModelsOnce an FM is translated into a suitable representationit is possible to use off–the–shelf solvers to automaticallyperform operations to analyse a FM [5, 6].The current implementation of the framework integratesthree of the most commonly used logic representations pro-posed for the automated analyses of feature models: CSP,SAT and BDD. A complete performance test of solversdealing with such representations and details about thetranslation of an FM into a CSP, SAT and BDD were in-troduced in [8, 5]. Following, we overview these represen-tations and we outline the most relevant performance detailsobtained from such test.2.1 Constraint Satisfaction Problem(CSP)A Constraint Satisfaction Problem (CSP) [17] consistson a set of variables, finite domains for those variables anda set of constraints restricting the values of the variables.Constraint Programming can be defined as the set of tech-niques such as algorithms or heuristics that deal with CSPs.A CSP is solved by finding states (values for variables) inwhich all constraints are satisfied. CSP solvers can dealwith numerical values such as integer domains. The mainideas concerning the use of constraint programming on FManalysis were stated in [5].Constraint Programming is the most flexible proposal. Itcan be used to perform the most of the operations currentlyidentified on feature models [6]. However, constraint pro-gramming solvers reveal a weak time performance when ex-ecuting certain operations on medium and large size featuremodels as for example calculating the number of possiblecombinations of features [7, 8].2.2 Boolean Satisfiability Problem (SAT)A propositional formula is an expression consisting on aset of boolean variables (literals) connected by logic opera-tors (¬, ∧, ∨, →, ↔). The propositional satisfiability prob-lem (SAT) [12] consists on deciding whether a given propo-sitional formula is satisfiable, i.e., a logical values can beassigned to its variables in a way that makes the formulatrue. The basic concepts about the using of SAT in the au-tomated analysis of FMs were introduced in [1].The performance results of SAT solvers are slightly bet-ter than the results of CSPs however this approach is not sopowerful [8]. To the best of our knowledge,