Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A. Statistical analysis of probabilistic models of software product lines with quantitative constraints. Extended Version. Technical report, 2015.
We investigate the suitability of statistical model checking techniques for the analysis of probabilistic models of software product lines with complex quantitative constraints and advanced feature installation options. Such SPL models are defined in the probabilistic feature-oriented language QFLan. QFLan is a rich process algebra whose operational behaviour interacts with a store of constraints and as such it allows to separate product configuration from product behaviour. The resulting probabilistic configurations and behaviour converge seamlessly in a semantics based on discrete-time Markov chains, thus enabling quantitative analysis. To this aim, we combine a Maude implementation of QFLan, integrated with Microsoft's SMT constraint solver Z3, with the distributed statistical model checker MultiVeStA. This enables analyses that range from the likelihood of specific behaviour to the expected average cost of products, in terms of feature attributes. We illustrate our approach by performing quantitative analyses on a bikes product line case study.
URL: http://milner.inf.ed.ac.uk/wiki/pages/J8N4c8/QUANTICOL_Technical_Reports.html
Subject Software Product Lines
Probabilistic Models
Quantitative Constraints
Statistical Model Checking
D.2.4 Software/Program Verification. Formal methods
D.2.4 Software/Program Verification. Model checking
D.2.4 Software/Program Verification. Statistical methods
D.2.13 Reusable Software. Domain engineering
F.3.2 Semantics of Programming Languages. Process models
G.3 Probability and Statistics

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional