Managing and Analysing Software Product Line Requirements
This addresses the problem of imprecise feature modeling for software product line developers, but it is incremental as it builds on existing UML and logic methods.
The paper tackles the lack of formal notations for modeling and verifying software product line variants by proposing an approach that uses UML for modeling and first-order logic for verification, validated with the Alloy tool on a Computer Aided Dispatch system.
Modelling software product line (SPL) features plays a crucial role to a successful development of SPL. Feature diagram is one of the widely used notations to model SPL variants. However, there is a lack of precisely defined formal notations for representing and verifying such models. This paper presents an approach that we adopt to model SPL variants by using UML and subsequently verify them by using first-order logic. UML provides an overall modelling view of the system. First-order logic provides a precise and rigorous interpretation of the feature diagrams. We model variants and their dependencies by using propositional connectives and build logical expressions. These expressions are then validated by the Alloy verification tool. The analysis and verification process is illustrated by using Computer Aided Dispatch (CAD) system.