Configuration of Non-Functional Properties in Embedded Operating Systems efforts. This technique is comparable to our idea of partial configuration. However, in contrast to our work, they state that the design stage is a good point to assure that the quality attributes are met. TOOL SUPPORT pure::variants (Beuche, 2003) is a tool that sup- ports variant management of SPLs. It is indepen- dent of programming languages and it enables the definition of the problem domain by means of feature models, and the solution domain by family models. It also automates the process of product generation. Regarding the configuration of NFPs, the current version is able to assign bugs (from a bug-tracking system) to specific features. Therefore, during product configuration, the ap- plication engineer is informed about the known bugs that will be present in the final product. Gears (Krueger, 2007b) is a tool and framework that enables the development and evolution of SPLs; it applies the three-tiered SPL methodology (Krueger, 2007a). In Gears, SPLs are comprised of three elements, software assets (source code, documentation, etc.), product feature profiles (to model each product in the portfolio), and the Gears configurator, which automatically assembles products based on their specifications. FeaturePlugin (Antkiewicz and Czarnecki, 2004) is an open-source Eclipse plugin for design- ing and configuring feature models. It supports the concepts of staged configuration (Czarnecki et al., 2005b) and feature cardinalities (Czarnecki et al., 2005a). The tool focuses on providing advanced techniques of feature modeling and not on sup- porting the whole process of SPL development. FAMA (FeAture Model Analyser) (Benavides et al., 2007) is an extensible framework for the automated analysis of feature models. It is able to denote feature models in several logic representa- tions; therefore, different solvers can be used in the analysis process. Currently, it supports CSP, SAT (boolean satisfiability problem), and BDD (binary decision diagrams), but it is flexible enough to have other solvers added to it. Cardinality-based feature models are allowed and the following operations are supported: finding out if a feature model is valid (there exists a valid selection that satisfies all constraints), finding the total number of valid products, listing all valid configurations, and calculating the commonality of features (the number of valid products they appear in). There are commercial, free, and open-source alternatives for the design of feature models. However, only pure::variants is able to provide non-functional information during product con- figuration; at the moment only at a very basic level, though. REASONING IN FEATURE MODELS Important to our work is also the process of reasoning in feature models. A seminal work by Benavides et al., (2006) presents the mapping from feature model components (e.g., optional features, mandatory features, and group features) to diverse logical representations, namely SAT, BDD, and CSP. Transforming feature models in these representations enables the use of off-the- shelf solvers that can perform several analyses that are relevant for feature models (e.g., validity, number of solutions, etc.). The relation of feature models and grammars has also been studied (Batory, 2005). Batory, also motivated by the ability to use off-the-shelf satisfiability solvers, presented the mapping from feature models first to iterative tree grammars, and then to propositional formulas. However, his main goal was to simplify the laborious task of debugging feature models. Recently, the relation of feature models and logic representation has been further explored. (Czarnecki and Wasowski, 2007) propose a method for the inverse transformation from propo- sitional formulas to a feature model representation. (Janota and Kiniry, 2007) study the representation 99