Logic Verification of Product-Line Variant Requirements
This provides a precise verification method for software product line developers, though it is incremental as it applies existing logic to a specific domain.
The paper tackled the lack of a formal notation for verifying product-line variant requirements by modeling feature diagrams using first-order logic, enabling validation with verification tools, as demonstrated in a case study of a Computer Aided Dispatch system.
Formal verification of variant requirements has gained much interest in the software product line (SPL) community. Feature diagrams are widely used to model product line variants. However, there is a lack of precisely defined formal notation for representing and verifying such models. This paper presents an approach to modeling and verifying SPL variant feature diagrams using first-order logic. It 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. A case study of a Computer Aided Dispatch (CAD) system variant feature model is presented to illustrate the verification process.