Model Checking for Software Product Lines with SNIP

Andreas Classen 1, * Maxime Cordy 2, * Patrick Heymans 3, 4, 5, * Pierre-Yves Schobbens 2 Axel Legay 6
* Auteur correspondant
2 PReCISE
PReCISE - PReCISE Research Centre in Information Systems Engineering
3 ADAM - Adaptive Distributed Applications and Middleware
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
5 PReCISE
Université de Lille, Sciences et Technologies, PReCISE - PReCISE Research Centre in Information Systems Engineering
6 DISTRIBCOM - Distributed and Iterative Algorithms for the Management of Telecommunications Systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We present SNIP, an efficient model checker for software product lines (SPLs). Variability in software prod- uct lines is generally expressed in terms of features, and the number of potential products is exponential in the number of features. Whereas classical model checkers are only capa- ble of checking properties against each individual product in the product line, SNIP exploits specifically designed algo- rithms to check all products in a single step. This is done by using a concise mathematical structure for product line behaviour, that exploits similarities and represents the behav- iour of all products in a compact manner. Specification of an SPL in SNIP relies on the combination of two specification languages: TVL to describe the variability in the product line, and fPromela to describe the behaviour of the individ- ual products. SNIP is thus one of the first tools equipped with specification languages to formally express both the variabil- ity and the behaviours of the products of the product line. The paper assesses SNIP and suggests that this is the first model checker for SPLs that can be used outside the academic arena.
Type de document :
Article dans une revue
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2012, 〈10.1007/s10009-012-0234-1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00717956
Contributeur : Patrick Heymans <>
Soumis le : samedi 14 juillet 2012 - 17:53:13
Dernière modification le : vendredi 16 novembre 2018 - 01:23:57

Lien texte intégral

Identifiants

Citation

Andreas Classen, Maxime Cordy, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay. Model Checking for Software Product Lines with SNIP. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2012, 〈10.1007/s10009-012-0234-1〉. 〈hal-00717956〉

Partager

Métriques

Consultations de la notice

593