Compositional Verification of Software Product Lines

International audienceWe present SPLEnD, the first compositional design verification engine for evolving software product lines(SPLs). The unique aspect of SPL development is the reuse of common features and management of variability among the family of products. The proposed design verification engine assumes that each SPL is composed of multiple features with each feature exhibiting variability. One novel aspect of SPLEnD is that it enables verification of SPLs, in which the variability information is captured differently at different levels of abstractions in the design and requirement stages. Another novel aspect of SPLEnD is that it enables compositional verification of designs against requirements. This involves first verifying the individual features separately, which provides a mapping between the variabilities at the requirement and design levels. The obtained mapping relations are then combined in the second step to check the conformance of the entire SPL. Feature level verification essentially involves standard model checking, while for the second step, a Quantified Boolean Formula (QBF) is synthesized and solved. The QBF avoids the explicit enumeration of all possible products thereby reducing the verification effort greatly. SPLEnD uses SPIN for the first step while the state of the art QBF solver CirQit is used for the second step. Thanks to the compositionality, SPLEnD easily handles the evolution of SPL by addition of new features and modification of existing features. Experimental results with SPLEnD look very promising: SPLs with several thousands of features were verified efficiently. A video of SPLEnD can be seen at http://www.cse.iitb.ac.in/$\sim$krishnas/splend.swf or http://www.cse.iitb.ac.in/$\sim$krishnas/splend.avi