Symbolic Model Checking of Software Product Lines

Abstract : We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2 n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics. We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one. In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm.
Type de document :
Communication dans un congrès
ICSE 2011 : 33rd International Conference on Software Engineering, Jun 2011, Honolulu, United States. pp.321-330, 2011, 〈10.1145/1985793.1985838〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087657
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 15:01:10
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 14 avril 2017 - 19:19:40

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay. Symbolic Model Checking of Software Product Lines. ICSE 2011 : 33rd International Conference on Software Engineering, Jun 2011, Honolulu, United States. pp.321-330, 2011, 〈10.1145/1985793.1985838〉. 〈hal-01087657〉

Partager

Métriques

Consultations de la notice

366

Téléchargements de fichiers

355