Today's systems are often highly con gurable requiring to model them as product lines. For this, feature modeling has been developed to capture the aspects of commonality and variability of systems, which are then represented as con gurations of feature models. Validating such con gurations is therefore an important topic. Yet, existing approaches have several limitations such as scalability issues for large systems and system families and cannot handle the di erent feature modeling language variants or extensions that have been proposed.
We present our ongoing work on a novel approach to validate feature model con gurations by translating them to Petri Nets. The approach can handle extended models of extended feature modeling languages and proposes an incremental validation scheme.
We detail the major steps of our approach using a simple example Feature Model depicted in Fig. 1(a). The example Feature Model has 8 features from A to H, with A as the root feature. Other than the feature-relationships that are apparent from the gure, there exists a cross-tree constraint (B =) C) and a cardinality constraint h1; 3; A; Di. B; E are dead-features and D; H are falseoptional.
Transformation: The transformation from Feature Model to Petri net has been developed to construct a constraint satisfaction problem from the constraints of the feature model. Features are mapped to unique places and featurerelations/constraints are mapped to unique transitions. The functions associated with the out-going edges (in yellow) are the key take-away from this section. These functions consist of a multiplication of two terms. The multiplier is a Boolean condition (within []) type-cast to integer. The Boolean conditions, are designed so that \when a transition is red, if the con guration does not satisfy the constraint represented by the transition, the values of the tokens in all the corresponding post-places are modi ed"4. The multiplicand has been designed to preserve the cardinality of the feature and corresponding token. In a con guration, for each feature, there is a token in the corresponding place with the same corresponding value as the cardinality in the con guration.
Validation: The veri cation of a feature con guration follows from the logic used in de ning the functions associated with the output-arcs. To do so, all Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 4 derivation methodology for the out-going function corresponding to each featurerelation and constraint available at https://github.com/raks0009/FM2PN corresponding transitions (constraints) are red (tested). If there is a change in the marking of the Petri net, the particular transition ( ring which results in a change in the marking) is associated with a constraint that is not satis ed by the con guration. The transition is agged for the user to rectify. If the values associated with all features in the con guration are compliant, the algorithm terminates without any ags, and the con guration is validated.
In the motivating example, the described approach tells the user that the ring of transitions t3 and t7 results in a change in the marking. Transition t3 corresponds to the `AND-optional' feature relation between B and E. In the con guration, E is selected but B is not, which is incorrect. Similarly, transition t7 corresponds to the cardinality constraint between A and D which speci es that for every instance of A there can be minimum 1 and maximum 3 instances of D. A has the cardinality 1 and D has cardinality 4 in the con guration which does not follow this constraint, hence the transition is agged.
Advantages and Limitations: The proposed approach can handle validation
of feature con gurations that adhere to extensions of feature models, something
that is relatively unexplored in the literature [