Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking

TL;DR

This paper explores the use of statistical model checking for analyzing probabilistic properties of software product line models, introducing an enriched language and applying it to a case study.

Contribution

It introduces PFLan, an extension of FLan with probabilistic features, and demonstrates its application with statistical model checking for quantitative analysis.

Findings

Successfully modeled probabilistic software product lines using PFLan.

Performed quantitative analysis of behavior likelihoods and costs.

Validated the approach with a case study on a simple product line.

Abstract

We investigate the suitability of statistical model checking techniques for analysing quantitative properties of software product line models with probabilistic aspects. For this purpose, we enrich the feature-oriented language FLan with action rates, which specify the likelihood of exhibiting particular behaviour or of installing features at a specific moment or in a specific order. The enriched language (called PFLan) allows us to specify models of software product lines with probabilistic configurations and behaviour, e.g. by considering a PFLan semantics based on discrete-time Markov chains. The Maude implementation of PFLan is combined with the distributed statistical model checker MultiVeStA to perform quantitative analyses of a simple product line case study. The presented analyses include the likelihood of certain behaviour of interest (e.g. product malfunctioning) and the expected average cost of products.