Analysis of Feature Models Using Alloy: A Survey

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 our paper Analysis of Feature Models Using Alloy: A Survey, presented at FMSPLE’16 (the 7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering), 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 of its kind comparative study of research targeted towards using Alloy for FM analysis. This review, written by Anjali Sree-Kumar, Elena Planas and Robert Clarisó, aims to identify the best practices on the use of Alloy. This work is part of a framework for the automated extraction and analysis of rich FMs from natural language requirement specifications.

You can also take a look at the presentation:

You can also read the full paper here or continue reading below (apologies in advance for the quality of the text, it is been automatically generated from the .tex sources). And as always, we’ll be very happy to know what you think about this work.

1 Introduction

Many software systems are not one-of-a-kind, but a family of related products in a given application domain called software product line (SPL). Products in a SPL can be differentiated by their features, defined as “increments in program functionality” [3] or “user-visible aspects or characteristics of the domain” [14].  Hence, modeling a SPL requires describing the features and the relationships among them such as dependencies or incompatibilities. That is, unlike traditional models of information systems (considering a single product), models of SPLs capture the variability among a family of products.

Feature Models (FMs) [4] are a popular family of notations, capable of describing complex SPLs. FMs can be constructed for a given application domain, using a methodology known as Feature-Oriented Domain Analysis (FODA) [14]. The output of this process is a FM, a diagram describing a complete SPL as a set of features and relationships. The diagram looks like a connected graph with the boxes/nodes in the diagram representing Features, edges representing relationships, and cross-tree constraints expressed as Propositional logic formulas.  A product becomes a configuration of this diagram, i.e. a subset of features that satisfies all the relationships and constraints.  Throughout this paper we will use product configuration, product and configuration with interchangeable meanings.

Given an FM, it is important to detect potential defects, e.g. no valid product, dead features (that cannot appear in any product), false optional features (that are required in every product), etc.  For instance, the FM illustrated in Fig. 1 is the model of a vending machine product line.  A cross–tree constraint makes HotWater a required feature when the features Tea or Soups are selected in the FM. This makes Soups unselectable in any configuration as the Dispenser can either have Beverages or Soups but never both. Meanwhile, optional feature HotWater is required by mandatory feature Tea (making it mandatory).

Figure 1: The vending machine FM created in FeatureIDE [15].

There are several techniques and tools that have been considered for this purpose, as surveyed in [4]. Among these tools, a popular choice is Alloy [13], a light-weight formal modeling language with an efficient model finder.  The generic semantics and versatility of the relational logic used in Alloy together with a fully automated analysis [25] makes Alloy an ideal choice for building complex automated tools based on it.  Other options include Description Logic based and Constraint programming based approaches as illustrated in the survey by Benavides et al. [4].

The differences among the existing research works using Alloy lie in the formalization of the FM. Different formalizations provide unique benefits, e.g. readability or efficiency of the analysis. However, there is a lack of information regarding the relative merits of each proposal, making it difficult to select the most suitable one for a specific type of analysis. In this paper, we review the state of the art in the analysis of FMs using Alloy. Our goal is to characterize the strengths and weaknesses of various Alloy encoding approaches from several perspectives such as expressivity of the FM, efficiency of the analysis, existence of tool support, etc.

2    Background

In this section we briefly discuss the existing surveys on this research subject. Then, we present a short summary of the required technical knowhow about Alloy and FM in general with an introduction to the benchmark FM. The section concludes with a short overview of the specific FM analysis operations that are considered by various research papers.

2.1 Related surveys

There are 3 surveys [4, 16, 24] which have systematically studied the state-of-the-art on FM analysis. Most of the high level findings related to tools support and capability of executing analysis operations have been documented in those surveys, but with no specific focus towards using Alloy as the analysis tool. Benavides et al. [4] have consolidated a complete list of analysis operations which are fundamentally required for a fully operational end-to-end FM analysis automated tool. We have used this list as our reference to evaluate the support levels extended by the different papers that are reviewed during this survey.

2.2   Benchmark feature  model

For comparing the selected research works, a suitable FM has to be set as the benchmark. We have used the bCMS software product line [6, 21] (see Fig. 2) for this purpose. The bCMS-SPL is a case study defined for the Workshop on Comparing Modeling Approaches (CMA’2011). It describes a family of car crash emergency systems in a FM with 28 features and 30 relationships among features. Two of these relationships are simple (at most 2 features involved) cross–tree constraints.

2.3   Alloy semantics

In Alloy, a model is described as a collection of signatures (sig), which identify the potential types for objects. Signatures can have fields with values like references to other objects, sets of objects or mappings among objects. Facts (fact) are constraints that capture the well-formedness rules of the model. Then, it is possible to check two types of properties:  assertions (assert), i.e.  searching an instance that violates a condition, or predicates (pred), i.e.  searching an instance that fulfills it.  When defining complex facts, predicates or assertions, it is possible to use functions (fun) to reuse and encapsulate large sub-expressions.

Properties can be expressed using a relational logic that combines features from first-order logic (quantifiers and Boolean operators), set operations (navigations through references and mappings) and the operators of relational calculus (e.g. computing the differences among two relations).

Figure 2: The bCMS FM [21] created using FeatureIDE [15].

2.4   Analysis operations

In order to evaluate each encoding and the analysis operations supported by them, we have listed all the operations as described by Benavides et al. [4] across Table 1 (which lists out only those operations which are included in one or more research works considered in the survey). More explanations on the importance and relevance of each analysis operation can be found in [4].

Table 1: FM analysis operations commonly found across multiple research works.

Id	Operation	Analysis operation description	Supported by
A1	Void FM	A feature model is void if it represents no products	[12, 19, 20, 26]
A2	Valid product	A product is valid if it belongs to the set of products defined by the FM	[1, 7, 10–12, 19,20, 23, 26]
A3	All products	All valid products possible from the FM	[11]
A4	Filter	For a given partial product configuration this analysis will result in a list of valid products that can be generated from this partial configuration	[1]
A5	Dead features	A feature is dead if it cannot appear in any of the products of the SPL	[10, 11]
A6	Wrong  cardi-nalities	These appear in cardinality-based feature models where cross-tree constraints are involved. A group cardinality is wrong if it cannot be instantiated	[1]
A7	Refactoring	An FM is a refactoring of another one if both represent the same set of products while having a different structure	[26]
A8	Commonality	This operation takes an FM and a configuration as input and returns the percentage of products represented by the model including the input configuration	[1]
A9	Variabilityfactor	This operation takes an FM as input and returns the ratio between the number of products and 2n where n is the number of features considered.	[14]
A10	Degree of or-thogonality	This operation takes an FM and a subtree (represented by its root feature) as input and returns the ratio of the total number of products of the FM and the number of products of the subtree	[1]

3    Review method

The review begins by considering existing surveys (e.g. [4, 16, 24]) and searching the following terms using a logical and operator for the combination, in the abstract and keyword lists of the following scientific databases:

• Search terms:  Feature Model, Alloy, analysis, software product line, verification
• Data sources: IEEE Xplore, ACM Digital Library, ISI Web of Knowledge

The search process is iterated on the list of bibliographic references in each of the identified papers, in order to identify any potentially missing references.  Overall, this initial search produced 47 research papers. Fig. 3 presents a timeline of these references.

In order to refine this collection of references, Table 2 describes the inclusion and exclusion criteria used to select only the specific works related to our survey interest. On one hand, we focus on works dealing with the analysis of FMs following the Feature-Oriented Domain Analysis (FODA) conventions.

Figure 3: Collected papers statistics.

Table 2: Selection criteria used in this literature review.

Inclusion criteria	Exclusion  criteria
1. Discusses FM properties that can be analyzed using Alloy2.  Focuses on Alloy-based Feature Model analysis of SPLs3. Introduces a new FM encoding or improve/extend existing encoding to include a new analysis	1. Does not consider FODA-style FMs describing a SPL2. Does not consider the analysis of the FM3. Does not use Alloy as the underlying verification engine

[14].  On the other hand, methods that include information beyond Feature Models, e.g. behavioral models [8] or use-case models [2], are omitted. As it is shown in Table 2, we only consider papers using Alloy as the verification engine. Thus, we omit any paper that uses alternative formalisms (e.g. constraint programming or description logic) or any other propositional logic provers [4, 16].

After applying the inclusion and exclusion criteria from Table 2, the final set of selected papers consists of 9 research papers which qualified to be included for our detailed review process.  These papers from 2005 until 2015 include: 6 papers from conference proceedings [7, 12, 19, 20, 23, 26], 2 from journal publications [1, 10] and 1 technical report [11].

3.1   Threats to validity

Before we go on further with the details of this literature survey, we would like to identify a set of potential weaknesses in our review process:

• We have not included all possible list of literature databases, e.g. DBLP or Google scholar. On the other hand, the considered surveys [4, 16, 24] are very recent (2010, 2014, 2015), and so they offer a good coverage of recent works.

• Other combinations of equivalent terms, such as “variability modeling”, “automated FM analysis”, etc. have not been considered. As a result of our search, and to the best of our knowledge, these nine selected papers are the most relevant for the topic addressed in this review.

• Marcilio et al. [18] and Liang et al. [17] have been successful in evaluating SAT-based FM analysis on very large FMs such as the FM of Linux kernel (5814 features), and found that the results were promising in terms of scalability of the FM and solver execution times. All such evaluations were done on FMs represented in Conjunctive Normal Form (CNF) which can be fed as input to SAT solvers such as the SAT4j standalone SAT solver. In this paper we could not use such very large FMs in CNF format mainly because we lacked the tool support for converting such CNF notations into Alloy specifications.  Moreover it would be difficult to validate the results of analysis of various FM analysis operations on such large FMs. Therefore the scalability of Alloy encoding for larger FM specifications and its performance with respect to analysis execution time for such large FMs has not been covered in this paper.

• We did not quantify the encoding performance in terms of the time taken to manually convert any FM to Alloy specification (ease of use).

• As there is only one case study the respective merits of each encoding may vary on different FMs.

4    Evaluation

Our review was intended towards answering the following research questions for each selected work:

1. What is the goal of FM analysis, i.e. is there a motivating scenario?
2. What degree of expressivity is supported in the FM, i.e. what kind of relationships are allowed?
3. What kind of analysis can be performed on the FM? What is the efficiency of those analysis?
4. What kind of tool support is available for generating the Alloy specification automatically?

4.1   Formalization strategies

This subsection provides an overview of the general formalization of FMs in the Alloy notation, in order to facilitate the comparison among the different formalization strategies. All selected works use common conventions in their Alloy encodings. For instance, all works share common concepts among the signatures they declare: Feature, Relationship and Configuration.  A Feature represents a major functionality of a software product.  Relationships are connections between features.  Most connections are between a complex feature (parent) and its set of sub-features (children), defining a tree- like structure. However, it is possible to define cross-tree relationships connecting arbitrary features, for example, stating that a feature requires another feature. Finally, a Configuration (also called Concept in [26]) is a set of features that define a product of an SPL.

4.2   Goal of analysis

The goal of FM analysis in general should be to identify all sorts of problems (like dead features, presence of false optional features etc.)  in the FM and suggest corrective measures to make the FM valid.  For example, if we consider the Vending machine FM shown in Fig. 1 it has both dead features and false optional features. Both these problems can be resolved if a ’Refactoring’ (A7) FM analysis operation is applied and the structure of the FM is changed to Fig. 4. This FM is found to be completely valid with 162 possible product configurations (as calculated by FeatureIDE [15]). In our survey, every selected research work was targeting to emphasize on some or the other analysis operation on the feature model. The most common analysis operations are:  check if an FM is void (A1) [12, 19, 20, 26], finding invalid/valid configurations (A2) [1, 7, 10–12, 19, 20, 23, 26] and finding dead features (A5) [10, 11].  The support extended for each analysis operation by the different selected papers in our review, has been marked under the Supported by column of Table 1.

Figure 4: The corrected vending machine FM created in FeatureIDE [15].

4.3   Degree of expressiveness

Expressivity has been evaluated in terms of the ability to encode all possible relationships and constraints between features in the Alloy notation. We have consolidated all such relationships and constraints and tabulated them under the Relationships sub–table of Table 3.  This table shows that some papers lack support for some types of relationships in the FM. This was purely a choice of the respective authors, considering only the properties of interest and a trade-off between expressivity and efficiency.

4.4   Efficiency of the analysis

To measure the efficiency, we have compared the execution time for various analysis operations using version 4.2 of the Alloy Analyzer (using the default SAT4j solver [5]). We have used the Alloy encoding proposed by each paper to model the bCMS FM and then performed different analysis operations. Also note that we have not included any evaluation of the analysis performance compared to other verification engines beyond the Alloy Analyzer.

The details of the execution time in milliseconds can be found in Table 3.

4.5   Available tool support

Regarding the source of the FMs, there is no standard textual format to represent FODA style feature models.  Hence, all works start from a manually created FM. In some cases [1, 7, 10–12, 23], the FM is a formal specification created specifically for analysis purposes. In others [19, 20, 26], the FM is the manual translation of the requirements document of a SPL.

Regarding the generation of the Alloy specification from the FM, the inference was again that there was a lack of tool support: only Nakajima et al. [19] have a prototype tool called FD-Checker that can generate the Alloy specification from a propositional logic formula. All the other papers do not have any kind of tool support, so the Alloy formalization needs to be generated manually. In our opinion, this is a significant finding in this literature survey. This has also made it very difficult for us to evaluate the research results of the bCMS case study, as it involved manual translation of FM specifications to the respective Alloy encoding.

For each reference (1st row) in Table 3 the set of supported relationships in the FM, i.e. their expressivity (2nd row), the availability of tool support for automatically generating the formal Alloy specification (3rd row) and the set of analysis operations offered by each method and its efficiency (4th row) in terms of the execution time for each analysis, has been summarized.

5    Discussion

In the following subsections we discuss the details of each encoding approach followed by the different research papers considered in this review in chronological order. Each research paper corresponds to one approach, also referred to as one strategy.

5.1   Alloy encoding and analysis of bCMS FM

In this subsection we include all major findings related to each selected paper and would provide the information based on the following criteria:

• Overview of the encoding strategy used – Specialty of the encoding and identifying the distinguishing aspect of the strategy.

• Strengths and limitations of the encoding – Comparison with the encoding described by other research papers.

• Ease of reproducing the research results – Discusses the effort to encode the bCMS FM and perform the analysis operations.

• Major technical roadblocks – Discusses the technical limitations and roadblocks that were encountered while reproducing the analysis results on the encoded bCMS FM.

Wang et al. [26]: The encoding is thoroughly described in the paper.  This is the only encoding which is able to perform a check for semantic equivalence between an FM and its refactored model. Unlike other papers this approach did not discuss about finding dead features, finding all possible product configurations or provide explanations for analysis results. The encoding was easy to reuse for the bCMS FM and the results stated in the paper were completely reproduced without any technical issues.

Gheyi et al. [11]: Gheyi proposed two theories for Feature Model analysis, the R-Theory and the G- Theory. The R-Theory defined a FM as a set of features. The G-Theory was a concise approach towards creating reusable constructs that are generically implemented in order to allow easy FM specification in Alloy. The encoding was more mature than the specifications of Wang et al. [26] in terms of expressivity as it was the only encoding among the surveyed papers that supported finding all valid products from any FM. It was easy to generate Alloy specifications for bCMS FM. FM analysis such as checking for valid/invalid product configurations, identifying dead features and collecting all valid product configurations was performed on bCMS FM and the results are presented in Table 3. A major roadblock in the implementation of these theories in Alloy for the bCMS FM was the use of logical constructs (recursion) that are unsupported by the current version of the Alloy notation. This was resolved when we directly contacted the authors and got a solution from them.

Tanizaki  et al. [23]: The encoding described in this paper is the most difficult to understand as the semantics used is very different from what we have seen in all the other approaches. Here the concept of a Feature-Model-Connection has been introduced in order to support traceability of configuration changes in a software system.  The time taken to specify the bCMS FM was thrice the time what we took for the other encodings. The main roadblock was in understanding the encoding in terms of FM analysis as they were mainly targeted towards backtracking FM changes to identify any new invalid FM state.  This is more or less a combination of analysis properties A12 & A13. But we were unable to reproduce the research results. This was mainly because of a lack of clarity in the encoding (too many signatures with no reusable functions or predicates which can aid in specifying bCMS FM in Alloy) encoding and incomplete encoding information in the paper (finding a product instance using the address book example from the paper was not directly reproduced because of the missing encodings which the authors have explicitly mentioned of having excluded it from the paper).

Nakajima  et al. [19]: The most remarkable aspect of this encoding is that the features and its relationships are all encoded in terms of propositional logic formulas (using many sig and fact), rather than using the fun or pred constructs of Alloy. This makes the encoding effort for very large FMs a time consuming and error-prone process. The major strength of this encoding lies in its direct and simple to understand encoding semantics. But unfortunately this approach has a very long running time for the A2 analysis operation (see Table 3) even for such a small sized FM. Unlike Gheyi et al. [11], this encoding is not very compact while it is more flexible and potentially easier to be generated automatically for any given FM. For this reason, they had introduced a tool called FD-Checker which could have been useful to convert propositional logic formulas to Alloy specifications of the FM. Nevertheless, the tool is currently not available in the public domain and we did not contact the authors as we were working on a smaller FM which we managed to encode manually.

Finkel et al. [10]: The goal of this paper was to detect all possible configurations and find if the model has any optional-feature flaw and missing-feature flaw.  If a feature is marked as optional but exists in all valid products from the FM, then the FM is said to have an optional-feature flaw. Whereas, in the same way if a mandatory feature is absent in all products then the FM has a missing-feature flaw. For specifying the bCMS FM we had to manually encode the features as different signatures and specify relationships as propositional logic formulas in Alloy, similarly to Nakajima et al. [19]. Therefore the encoding was simple and easy to reproduce but it was time consuming and error-prone. This calls for automated tools to support the translation of FM to Alloy specifications.

Ripon  et al. [20]:  The main objective of this paper was to present an approach for formalizing and verifying SPL FMs with support for automatically generating customized products based on user requirements.  They have used the same Alloy encoding as described by Gheyi et al. [11] in their G- Theory and Wang et al. [26], and hence have similar findings.  This can be seen from the results of analysis in Table 3.

Huang et at. [12]: The encoding is very similar to Nakajima et al. [19] as they have extended the same encoding to include signatures (sig) that will enable analysis operations to check for valid/invalid sub–FMs in an FM. This approach is very verbose and error-prone due to relying completely on propositional logic formulas. Two analysis operations A1 & A2 are successfully performed using this encoding on bCMS. Though the authors have even mentioned about detecting valid/invalid sub–models that aid in refining the overall FM using Refactoring (A7), this was not explicitly demonstrated in the paper and hence it is not included in the bCMS analysis.

Jaime et al. [7]:  The objective of this paper was to detect conflicts in the product configuration process which occur when intended features cannot be selected because of other choices of features included into the product.  For this they have identified and included one more type of relationship which is ’Non-selectable’ in addition to the relationship encodings provided by Gheyi [11].  An FM is considered as invalid if full mandatory features that must be included in all the configurations are also non-selectable. The encoding was easy to understand and apply for specifying the bCMS FM. The analysis operation A2 took slightly more time compared to other approaches though the encoding was better encapsulated with appropriate predicates and functions for easy FM specification. There were no technical roadblocks.

Ajoudanian et al. [1]: Constraint-based FMs with cardinalities are known as extended feature mod- els. Hence they are feature models with attributes. This paper describes a promotion technique in Alloy which claims to significantly improve the efficiency of analysis operations performed on such extended Feature models. We were unable to reproduce the results of the paper using the example and Alloy specifications provided in it. When the Alloy encoding details were directly used, it showed several syntax errors in the Alloy editor such as missing ‘{’, ‘.’ between univ and ‘(’, undefined variables, invalid Alloy symbols for less than or equal and greater than or equal. Therefore it was difficult to reuse the encoding and reproduce their results with bCMS FM.

Table 3: Review summary on the analysis of FM using Alloy.

Reference	Wang[26]	Gheyi[11]	Tanizaki[23]	Nakajima[19]	Finkel[10]	Ripon[20]	Huang[12]	Jaime[7]	Ajoudanian[1]
Expressivity	R1-7	R1-3, R5	R1-3, R5-7	R1-7	R1-3, R5	R1-5	R1-3	R1-3, R5-7	R1-3, R5
Tool support	None	None	None	FD-Checker	None	None	None	None	None
Analysis*(Identifier + Execution time)	A1  5 msA2  7 msA7  1 ms	A5  25 msA2  20 msA3  30 ms	A2  10 ms	A1      8 msA2  610 ms	A2   7msA5  4 ms	A1  10 msA2    8 ms	A1  5 msA2  5 ms	A2  22 ms	A2  5 ms

* Execution time of each analysis reported on the bCMS case study of Fig. 2

Settings: PC with 16Gb RAM and a 3.4GHz processor. Alloy Analyzer version 4.2 (SAT4j SAT solver). The Alloy source files for the bCMS product line, encoded using each approach are available at : https://www.dropbox.com/s/wysbls64ictoofm/Alloy.zip?dl=0

Relationships

Id	Definition
R1	Mandatory(x):Feature x must appear if parent(x) is included
R2	Optional(x) or Optional Or(x):Feature x may or may not appear if parent(x) is included
R3	Alternative(X ) or XOR(X ):Exactly one feature xi ∈ X  must appear if parent(X ) is selected
R4	Optional Alternative(X ):At most one feature xi ∈ X  must appear if parent(X ) is selected
R5	Or(X ):At least one feature xi ∈ X  must appear if parent(X ) is selected
R6	Requires(x, y):Feature x must appear when feature y is included
R7	Excludes(x, y):Feature x and y cannot appear both

5.2   Review summary

The evaluation summary is illustrated in Table 3. After analyzing and comparing the execution time for different operations, we have identified the list of various encodings that can be used for the respective analysis operations based on the encoding efficiency and execution time. This is summarized in Table 4.

We have identified two types of shortcomings in this literature survey that dealt with papers dealing with the analysis of FMs using Alloy: theoretical limitations and practical limitations.

Table 4:  Analysis operation and best encoding strategy based on lowest execution time and highest expressiveness.

Analysis operation	Encoding strategy		Analysis operation	Encoding strategy
A1 (Void FM)	Wang et al. [26]		A6 (Cardinalities)	Supported in [1]*
A2 (Valid product)	Wang et al. [26]		A7 (Refactoring)	Wang et al. [26]
A3 (All products)	Gheyi et al. [11]		A8 (Commonality)	Supported in [1]*
A4 (Filter)	Supported in [1]*		A9 (Variability)	Supported in [1]*
A5 (Dead features)	Gheyi et al. [11]		A10 (Orthogonality)	Supported in [1]*

* These are discussed by Ajoudanian et al. [1] but we were unable to reproduce the results due to various reasons as explained in Sec. 5

Theoretical limitations.  Most encodings only support parent-child relationships and trivial requires/excludes cross-tree constraints. Furthermore, only one of the papers demonstrated the encoding to compute the entire set of products in the product line by extending support for checks such as counting the number

of valid configurations. There is a wide scope for improving the encodings to allow more expressivity so that the other missing analysis operations (among the list of 30 as shown in Table 5) can also be automated.

Practical limitations. There were several challenges in our attempts to replicate each approach in the bCMS case study.

Firstly, only Nakajima et al. [19] describe a tool to generate the Alloy specification automatically. Even though the tool is still available, it is not available for download and use. Therefore, almost at all times during the review process, the Alloy encodings had to be generated manually.

Furthermore, the encoding proposed by Ripon et al. [20] is not fully described.  This means that some significant encoding is not provided in the paper and is neither available online. Attempts to fill the missing gaps yielded results which did not conform to the expected output obtained for the same analysis in the rest of encodings.

Finally, none of the works provided a large-scale FM for experimentation. Even though some approaches [1] claimed being validated on FMs with hundreds of features, the examples are not available and authors did not respond to inquiries.

6    Challenges and Future Research

The major challenge lies in having future research works targeting to address the missing analysis operations (Table 5) using Alloy analyzer.  The analysis operations such as Valid partial configuration, Dependency analysis, Redundancies and Commonality analysis have great significance when it comes to the industrial application of FM analysis during real product development. With the available research results we cannot implement a fully operational FM analysis automated tool based on Alloy without these missing operations that are crucial for generating feature models with lesser defects. Furthermore, it would be challenging to study in detail, all the formal proposals for semantics of feature models and how Alloy could be used to support each one of that semantics. As a starting point we would refer to the works of Schobbens et al. [22] and Amador et al. [9]. From the summary, it can be inferred that some of the existing research results can be reused for specific analysis operations. Future research must focus to resolve all the limitations identified in our review.

7    Conclusions

The main contribution of our work is to highlight the importance of future research in the direction of supporting automated FM analysis using Alloy, by identifying the limitations in the current state-of-the- art research contributions.  In this paper we have selected, analyzed and compared the most relevant papers dealing with this subject. Several previous works have proposed the analysis of FODA-style FMs through Alloy. All formalizations but [11] are unable to reason about more than one product configuration. Lack of tool support for converting informal FM specifications to respective encodings is one of the major limitations identified during this survey. There are other practical issues that hinder the industrial application of these research results such as: out-of-date tools and Alloy formats, several syntactic errors in the Alloy specifications provided in the papers, lack of complete descriptions for the Alloy theories, lack of large-scale examples and a large number of analysis operations which are still not supported using Alloy. All this calls for future research to facilitate an efficient and automatic analysis of feature-based requirement specifications using Alloy.

References

[1]  Shohreh Ajoudanian & Seyed-Hassan Mirian Hosseinabadi (2015): Automatic promotional specialization, generalization and analysis of extended feature models with cardinalities in Alloy. Journal of Logical and Algebraic Methods in Programming 84(5), pp. 640 – 667, doi:10.1016/j.jlamp.2014.11.005.

[2]  Mauricio Alférez, Roberto E. Lopez-Herrejón, Ana Moreira, Vasco Amaral & Alexander Egyed (2014): Consistency Checking in Early Software Product Line Specifications – The VCC Approach 20(5), pp. 640–665, doi:10.3217/jucs-020-05-0640.

[3]  Don Batory, David Benavides & Antonio Ruiz-Cortes (2006): Automated Analysis of Feature Models: Challenges Ahead. Commun. ACM 49(12), pp. 45–47, doi:10.1145/1183236.1183264.

[4]  David Benavides, Sergio Segura & Antonio Ruiz-Cortés (2010): Automated analysis of feature models 20 years later: A literature review. Information Systems 35(6), pp. 615 – 636, doi:10.1016/j.is.2010.01.001.

[5]  Daniel Le Berre (2010): SAT4J solver. Technical Report. Available at http://www.sat4j.org.

[6]  Afredo Capozucca, Betty H. C. Cheng, Geri Georg, Nicolas Guelfi, Paul Istoan, Gunter Mussbacher, Sai Pradeep Mandalaparty & Ana Moreira (2012): Requirements Definition Document for a Software Product Line of Car Crash Management Systems. Technical Report, University of Nice Sophia Antipolis, I3S CNRS, Berlin, Heidelberg, doi:10.1007/978-3-642-16086-8.

[7]  Jaime Alberto Chavarriaga Lozano, Carlos Francisco Noguera Garcia, Viviane Jonckers & Rubby Casallas (2013): Supporting Multi-level Configuration with Feature-Solution Graphs – Formal Semantics and Alloy Implementation. Technical Report, Software Language Lab, Berlin.

[8]  David Dietrich, Pourya Shaker, Joanne M. Atlee, Derek Rayside & Jan Gorzny (2012): Feature  Interaction Analysis of the Feature-oriented  Requirements-modelling Language Using Alloy. In: Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa ’12, ACM, pp. 17–22, doi:10.1145/2427376.2427380.

[9]  A. Durán, D. Benavides, S. Segura, P. Trinidad & A. Ruiz-Cortés (2015):  FLAME: a formal framework for the automated analysis of software product lines validated by automated specification testing.  Journal Software and Systems Modeling, pp. 1–34, doi:10.1007/s10270-015-0503-z.

[10]  Raphael Finkel & Barry O’Sullivan (2011): Reasoning about conditional constraint specification problems and feature models.  Artificial Intelligence for Engineering Design, Analysis and Manufacturing 25, pp. 163–174, doi:10.1017/S0890060410000600.

[11]  Rohit Gheyi, Tiago Massoni & Paulo Borba (2006): A Theory for Feature Models in Alloy. In: Proceedings of the ACM SIGSOFT First Alloy Workshop, Citeseer, Portland, United States, p. 71–80, doi:10.1.1.295.4053.

[12]  Changyun  Huang,  Yasutaka  Kamei,  Kazuhiro  Yamashita  &  Naoyasu  Ubayashi  (2013):   Using  Alloy to  support  feature-based  DSL construction  for  mining software repositories. SPLC  ’13,  p.  86, doi:10.1145/2499777.2500714.

[13]  Daniel Jackson (2006): Software Abstractions: Logic, Language, and Analysis. The MIT Press.

[14]  Kyo Kang, Sholom Cohen, James Hess, William Novak & A. Peterson (1990): Feature-oriented  domain analysis (FODA) feasibility study. SEI, CMU.

[15]  Christian Kästner, Thomas Thüm, Gunter Saake, Janet Feigenspan, Thomas Leich, Fabian Wielgorz & Sven Apel (2009): FeatureIDE: A Tool Framework for Feature-oriented Software Development. In: Proceedings of the 31st International Conference on Software Engineering, ICSE ’09, IEEE Computer Society, Washington, DC, USA, pp. 611–614, doi:10.1109/ICSE.2009.5070568.

[16]  Uwe  Lesta,  Ina  Schaefer  &  Tim  Winkelmann  (2015):   Detecting  and  Explaining  Conflicts in  Attributed  Feature  Models.    Electronic Proceedings in  Theoretical Computer Science  182,  pp.  31–43, doi:10.4204/EPTCS.182.3.

[17]  Jia Hui Liang, Vijay Ganesh, Krzysztof Czarnecki & Venkatesh Raman (2015): SAT-based Analysis of Large Real-world Feature  Models is Easy.   In:  Proceedings of the 19th International Conference on Software Product Line, SPLC ’15, ACM, New York, NY, USA, pp. 91–100, doi:10.1145/2791060.2791070. Available at http://doi.acm.org/10.1145/2791060.2791070.

[18]  Marcilio Mendonca, Andrzej Wa˛sowski & Krzysztof Czarnecki (2009):  SAT-based Analysis of Feature Models is Easy.  In: Proceedings of the 13th International Software Product Line Conference, SPLC ’09, Carnegie Mellon University, Pittsburgh, PA, USA, pp. 231–240, doi:10.1145/1753235.1753267. .

[19]  Shin Nakajima (2010): Semi-automated Diagnosis of FODA Feature Diagram. In: Proceedings of the 2010 ACM Symposium on Applied Computing, SAC ’10, ACM, pp. 2191–2197, doi:10.1145/1774088.1774550.

[20]  Shamim Ripon, Keya Azad, Sk Jahir Hossain & Mehidee Hassan (2012): Modeling and Analysis of Productline Variants. In: Proceedings of the 16th International Software Product Line Conference – Volume 2, SPLC’12, ACM, New York, NY, USA, pp. 26–31, doi:10.1145/2364412.2364417.

[21]  Rick Salay, Michalis Famelis, Julia Rubin, Alessio Di Sandro & Marsha Chechik (2014):  Lifting Model Transformations to Product Lines. In: Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, ACM, pp. 117–128, doi:10.1145/2568225.2568267.

[22]  P. Schobbens, P. Heymans & J.C. Trigaux (2006): Feature Diagrams: A Survey and a Formal Semantics. In: Requirements Engineering, 14th IEEE International Conference, pp. 139–148, doi:10.1109/RE.2006.23.

[23]  H. Tanizaki & T. Katayama (2008): Formalization and Consistency Checking of Changes of Software System Configurations Using Alloy. In: Software Engineering Conference, 2008. APSEC ’08. 15th Asia-Pacific, IEEE, pp. 343–350, doi:10.1109/APSEC.2008.64.

[24]  Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer & Gunter Saake (2014):  A Classification and Survey of Analysis Strategies for Software Product Lines.  ACM Comput. Surv. 47(1), pp. 6:1–6:45, doi:10.1145/2580950.

[25]  Emina Torlak & Greg Dennis (2006): Kodkod for Alloy Users. Alloy Workshop.

[26]  Hai Wang (2005):  Formal Semantics and Verification for Feature  Modeling.  ICECCS’05, pp. 303–312, doi:10.1109/ICECCS.2005.48.