Ter Beek M. H., Legay A., Lluch Lafuente A., Vandin A. Quantitative analysis of probabilistic models of software product lines with statistical model checking. In: FMSPLE'15 - 6th International Workshop on Formal Methods for Software Product Line Engineering (London, UK, 11 April 2015). Proceedings, pp. 56 - 70. J.M. Atlee, S. Gnesi (eds.). (Electronic Proceedings in Theoretical Computer Science, vol. 182). EPTCS, 2015. |

Abstract (English) |
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. | |

URL: | http://eptcs.web.cse.unsw.edu.au/paper.cgi?FMSPLE15.5 | |

DOI: | 10.4204/EPTCS.182.5 | |

Subject | Software Product Lines Probabilistic Models Quantitative Analysis Statistical Model Checking Process Algebra Maude MultiVeStA D.2.4 Software/Program Verification. Formal Methods D.2.4 Software/Program Verification. Model checking F.3.1 Specifying and Verifying and Reasoning about Programs F.3.2 Semantics of Programming Languages G.3 Probability and Statistics |

1) Download Document PDF |

Open access Restricted Private