Statistical analysis of probabilistic models of software product lines with quantitative constraints. Extended Version.

Ter Beek Mh, Legay A, Lluch Lafuente A, Vandin A

Software product lines  Probabilistic models  Quantitative constraints  Statistical model checking 

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.