Simulation-Based Abstractions for Software Product-Line Model Checking

Maxime Cordy 1 Andreas Classen 1 Gilles Perrouin 1 Pierre-Yves Schobbens 1 Patrick Heymans 2, 3, 4, 1 Axel Legay 5, *
* Auteur correspondant
1 PReCISE - PReCISE Research Centre in Information Systems Engineering
2 ADAM - Adaptive Distributed Applications and Middleware
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
3 Université de Lille, Sciences et Technologies
4 LIFL - Laboratoire d'Informatique Fondamentale de Lille
5 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 : Software Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce life cycle costs and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. Model checking SPLs is more difficult than for single systems, since the number of different products is potentially huge. In previous work, we introduced Featured Transition Systems (FTS), a formal, compact representation of SPL behaviour, and provided efficient algorithms to verify FTS. Yet, we still face the state explosion problem, like any model checking-based verification. Model abstraction is the most relevant answer to state explosion. In this paper, we define a novel simulation relation for FTS and provide an algorithm to compute it. We extend well-known simulation preservation properties to FTS and thus lay the theoretical foundations for abstraction-based model checking of SPLs. We evaluate our approach by comparing the cost of FTS-based simulation and abstraction with respect to product-by-product methods. Our results show that FTS are a solid foundation for simulation-based model checking of SPL.
Keywords : Feature Abstraction Formal methods Simulation Model Checking Software Product Lines
Type de document :
Communication dans un congrès
Martin Glinz and Gail Murphy and Mauro Pezze. ICSE 2012 : 34th International Conference on Software Engineering, Jun 2012, Zürich, Switzerland. pp.672 - 682, 2012, 〈10.1109/ICSE.2012.6227150〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01087659
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 14:39:05
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : vendredi 27 février 2015 - 12:20:25

Fichier

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

Identifiants

Collections

INRIA | LIFL | IRISA | UNIV-LILLE3 | IRISA-D2 | UR1-UFR-ISTIC | UNIV-RENNES

Citation

Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, et al.. Simulation-Based Abstractions for Software Product-Line Model Checking. Martin Glinz and Gail Murphy and Mauro Pezze. ICSE 2012 : 34th International Conference on Software Engineering, Jun 2012, Zürich, Switzerland. pp.672 - 682, 2012, 〈10.1109/ICSE.2012.6227150〉. 〈hal-01087659〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

641

Téléchargements de fichiers

382

Contact


archive-ouverte@inria.fr