Model checking software product lines based on feature slicing

Feature model is a popular formalism for describing the commonality and variability of a software product line in terms of features. Feature models symbolise a presentation of the possible application configuration space, and can be customised based on specific domain requirements and stakeholder goals. As feature models are becoming increasingly complex, it is desired to provide automatic support for customised analysis and verification based on the specific goals and requirements of stakeholders. This paper first presents feature model slicing based on the requirements of the users. We then introduce three-valued abstraction of behaviour models based on the slicing unit. Finally, based on multi-valued model checker, a case study was conducted to illustrate the effectiveness of our approach.