Skip to Main content Skip to Navigation
Conference papers

Compositional Verification of Software Product Lines

Abstract : We 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$\sim$krishnas/splend.swf or$\sim$krishnas/splend.avi.
Complete list of metadatas
Contributor : Team Kairos <>
Submitted on : Monday, March 11, 2013 - 3:40:03 PM
Last modification on : Wednesday, October 14, 2020 - 4:23:44 AM

Links full text




Jean-Vivien Millo, S. Ramesh, Shankara Krishna, Ganesh Narwane. Compositional Verification of Software Product Lines. iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. pp.109-123, ⟨10.1007/978-3-642-38613-8_8⟩. ⟨hal-00799108⟩



Record views