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.
|Journal||Electronic Proceedings in Theoretical Computer Science|
|Publication status||Published - 2015|
|Event||6th Workshop on Formal Methods and Analysis in SPL Engineering - London, United Kingdom|
Duration: 11 Apr 2015 → …
Conference number: 6
|Workshop||6th Workshop on Formal Methods and Analysis in SPL Engineering|
|Period||11/04/2015 → …|