An Cardinality-based Domain Feature Model Verification Method

Cardinality-based feature modeling is a particular form of domain modeling, which extends the original feature modeling from FODA[2] with feature and group cardinalities, feature attributes, feature diagram references. The mechanism of Cardinality allows feature and constrain having many copies in application feature model during customization from domain feature model. However,the mechanism of Cardinality brings two problems in the application feature model verification. One problem is that additional constrains among features will lose their original semantics. As a result, we lose the capability of verifying whether a customizing result is a valid one based on the constrains among features. Another problem is that the efficiency of application feature model verification is dropped down by the great deal of feature clones and additional constrain copies in the customization.According to the problem we faced in the cardinality feature model verification, referenced domain feature model checking methods, and combined with additional constrain semantic information in the cardinality feature model, the paper propose an domain feature model verification method. The method resolves the model checking problem caused by the cardinality mechanism. The main contribution of the paper is as follows.By the analysis of relationship between features, the paper specific two types of additional constrain at first, namely binary constraints and composite constraints. And according to the information that required by the integrity of additional constraints semantic in customized feature model, the paper gives the Schema definition and the forms of expression corresponding to two types of additional constraints. Facilitate the verification of feature model using the method. For the second problem, based on the impact of additional constrain judgment with characteristics of feature and selected status, employed the sufficient condition of invalid constrain as criterion rule, the method exclude invalid additional constrain relationship before feature model checking. Thus reduce the complexity of model verification.The paper proposes validate rules and formal specification corresponding two types of additional constraints. In order to further improve the check efficiency and reduce time complexity, the paper introduces the BDD (binary decision diagram) mechanism.