Design variability verification in Software Product Lines

This paper proposes a novel notion called variability verification applicable to Software Product Lines (SPL). Variability is central to SPL and we have observed that variability is expressed differently at different levels of abstraction in the development flow of SPL. A natural problem in this context is the conformance of variability information expressed at different levels. Design variability verification, in particular, checks whether the variability expressed at the design level conforms to that at the requirement level. Unlike many existing approaches to SPL modelling, our work does not assume a single global view of variation points, even within the same level of abstraction. In our view, an SPL is a concurrent composition of features, where each feature exhibits independent variability. This enables incremental addition of variability. The procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. Feature level verification essentially involves standard model checking while, in the second step, a Quantified Boolean Formula (QBF) is synthesized and solved. The method has been implemented and demonstrated in a tool SPL Engine for Design Verification (SPLEnD) on a couple of fairly large case studies. SPLEnD uses SPIN tool for the feature level conformance, while the state-of-the-art QBF solver CirQit is used for the SPL level conformance. SPLEnD easily handles the evolution of SPL by addition of new features and modification of existing features. Experimental results with SPLEnD look very promising.