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. In: SPLC'15 - 19th International Software Product Line Conference (Nashville, TN, USA, 20-24 July 2015). Proceedings, pp. 11 - 15. ACM, 2015.
We investigate the suitability of statistical model checking for the analysis of probabilistic models of software product lines with complex quantitative constraints and advanced feature installation options. Such models are specified in the feature-oriented language QFLan, a rich process algebra whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour. The resulting probabilistic configurations and behaviour converge seamlessly in a semantics based on DTMCs, thus enabling quantitative analyses ranging from the likelihood of certain behaviour to the expected average cost of products. This is supported by a Maude implementation of QFLan, integrated with the SMT solver Z3 and the distributed statistical model checker MultiVeStA. Our approach is illustrated with a bikes product line case study.
DOI: http://dx.doi.org/10.1145/2791060.2791087
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