A propositional logic-based method for verification of feature models

The feature model is a domain/product-line oriented requirements model based on hierarchical structure and explicit variability modeling, and has been adopted by several important software reuse methods. However, with respect to the problem of verification of constraints on features and verification of partially customized feature models, these methods tend to be semi-formal and offer little formal assistance. In this paper, we propose a propositional logic-based method for the verification of feature models at different binding times. The most important characteristic of this method is that it integrates the logical verification with binding times, which makes it can be used to verify any partially customized feature models at any binding time (except run-time). In this method, constraints on features are formalized by logical sentences. Thus, the verification of feature models is converted into satisfaction problems in the logic. With this formal method, verification problems such as the detection of inconsistent constraints or the detection of conflicting or unnecessary binding resolutions can be automatically revealed.