Counterexample Guided Abstraction Refinement of Product-Line Behavioural Models

Abstract : The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse. We discuss in which cases a given abstraction should be used.
Type de document :
Communication dans un congrès
FSE 2014 : International Symposium on Foundations of Software Engineering, Nov 2014, Hong Kong, Hong Kong SAR China. ACM, pp.190-201, 2014, 〈10.1145/2635868.2635919〉
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-01087789
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 16:25:06
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 14 avril 2017 - 19:53:30

Fichier

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

Identifiants

Citation

Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens, Bruno Dawagne, et al.. Counterexample Guided Abstraction Refinement of Product-Line Behavioural Models. FSE 2014 : International Symposium on Foundations of Software Engineering, Nov 2014, Hong Kong, Hong Kong SAR China. ACM, pp.190-201, 2014, 〈10.1145/2635868.2635919〉. 〈hal-01087789〉

Partager

Métriques

Consultations de la notice

432

Téléchargements de fichiers

297