Statistical Model Checking for Product Lines

Abstract : We report on the suitability of statistical model checking for the analysis of quantitative properties of product line models by an extended treatment of earlier work by the authors. The type of analysis that can be performed includes the likelihood of specific product behaviour, the expected average cost of products (in terms of the attributes of the products’ features) and the probability of features to be (un)installed at runtime. The product lines must be modelled in QFLan, which extends the probabilistic feature-oriented language PFLan with novel quantitative constraints among features and on behaviour and with advanced feature installation options. QFLan is a rich process-algebraic specifi- cation language whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour. The resulting probabilistic configurations and probabilistic behaviour converge in a discrete-time Markov chain semantics, enabling the analysis of quantitative properties. Technically, a Maude implementation of QFLan, integrated with Microsoft’s SMT constraint solver Z3, is combined with the distributed statistical model checker MultiVeStA, developed by one of the authors. We illustrate the feasibility of our framework by applying it to a case study of a product line of bikes.
Type de document :
Communication dans un congrès
7th International Symposium, ISoLA 2016, Oct 2016, Corfu, Greece
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01406531
Contributeur : Nisrine Jafri <>
Soumis le : jeudi 1 décembre 2016 - 11:58:54
Dernière modification le : jeudi 15 novembre 2018 - 11:58:54
Document(s) archivé(s) le : lundi 20 mars 2017 - 19:41:42

Fichier

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

Identifiants

  • HAL Id : hal-01406531, version 1

Citation

Maurice H Ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin. Statistical Model Checking for Product Lines . 7th International Symposium, ISoLA 2016, Oct 2016, Corfu, Greece. 〈hal-01406531〉

Partager

Métriques

Consultations de la notice

313

Téléchargements de fichiers

75