Logic Based Verification of Software Product Line Feature Model

Abstract

Feature diagrams are widely used to model product line variant . Formal Verification of variant requirements has gained much interest in the software product line(SPL) community . However, there is a lack of precisely defined formal notation for representing and verifying such models. This report presents an approach to modeling and analyzing SPL variant feature by Logic Based and also First order logic. The logical representation provides a precise and rigorous formal interpretation of the feature diagrams. Logical expressions can be built by modeling variants and their dependencies by using propositional connectives. These expressions can then be validated by any suitable verification tool such as Alloy. A case study of two Feature Model (GPL & Hall Booking System) variant feature model is presented to illustrate the analysis and verification process.