  This paper presents a novel approach to the design verification of Software
Product Lines(SPL). The proposed approach assumes that the requirements and
designs are modeled as finite state machines with variability information. The
variability information at the requirement and design levels are expressed
differently and at different levels of abstraction. Also the proposed approach
supports verification of SPL in which new features and variability may be added
incrementally. Given the design and requirements of an SPL, the proposed design
verification method ensures that every product at the design level behaviorally
conforms to a product at the requirement level. The conformance 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.
The method has been implemented and demonstrated in a prototype tool SPLEnD
(SPL Engine for Design Verification) on a couple of fairly large case studies.
