# Compositional Verification of Software Product Lines

1 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
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 http://www.cse.iitb.ac.in/$\sim$krishnas/splend.swf or http://www.cse.iitb.ac.in/$\sim$krishnas/splend.avi.
Type de document :
Communication dans un congrès
Einar Broch Johnsen and Luigia Petre. iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. Springer, 7940, pp.109-123, 2013, Lecture Notes in Computer Science; Integrated Formal Methods. <10.1007/978-3-642-38613-8_8>
Domaine :

https://hal.inria.fr/hal-00799108
Contributeur : Team Aoste <>
Soumis le : lundi 11 mars 2013 - 15:40:03
Dernière modification le : lundi 5 octobre 2015 - 17:01:06

### Citation

Jean-Vivien Millo, S. Ramesh, Shankara Krishna, Ganesh Narwane. Compositional Verification of Software Product Lines. Einar Broch Johnsen and Luigia Petre. iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. Springer, 7940, pp.109-123, 2013, Lecture Notes in Computer Science; Integrated Formal Methods. <10.1007/978-3-642-38613-8_8>. <hal-00799108>

### Métriques

Consultations de la notice