Model Checking Lots of Systems

Abstract : In product line engineering, systems are developed in families and differences between family members are expressed in terms of features. Formal modelling and verification is an important issue in this context as more and more critical systems are developed this way. Since the number of systems in a family can be exponential in the number of features, two major challenges are the scalable modelling and the efficient verification of system behaviour. Currently, the few attempts to address them fail to recognise the importance of features as a unit of difference, or do not offer means for automated verification. In this paper, we tackle those challenges at a fundamental level. We first extend transition systems with features in order to describe the combined behaviour of an entire system family. We then define and implement a model checking technique that allows to verify such transition systems against temporal properties. An empirical evaluation shows substantial gains over classical approaches.
Type de document :
Communication dans un congrès
ICSE 2010 : 32nd International Conference on Software Engineering, Jun 2010, Cape Town, South Africa. pp.335 - 344, 2010, 〈10.1145/1806799.1806850〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01087654
Contributeur : Uli Fahrenberg <>
Soumis le : mercredi 26 novembre 2014 - 15:27:39
Dernière modification le : mercredi 11 avril 2018 - 02:01:23
Document(s) archivé(s) le : vendredi 14 avril 2017 - 20:28:47

Fichier

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

Identifiants

Citation

Andreas Classen, Patrick Heymans, Pierre-Yves Schobbens, Axel Legay, Jean-François Raskin. Model Checking Lots of Systems. ICSE 2010 : 32nd International Conference on Software Engineering, Jun 2010, Cape Town, South Africa. pp.335 - 344, 2010, 〈10.1145/1806799.1806850〉. 〈hal-01087654〉

Partager

Métriques

Consultations de la notice

337

Téléchargements de fichiers

658