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

Publication: Research - peer-reviewConference article – Annual report year: 2015

View graph of relations

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.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
Volume182
Pages (from-to)56-70
ISSN2075-2180
DOIs
StatePublished - 2015
Event6th Workshop on Formal Methods and Analysis in SPL Engineering - London, United Kingdom

Workshop

Workshop6th Workshop on Formal Methods and Analysis in SPL Engineering
Number6
CountryUnited Kingdom
CityLondon
Period11/04/2015 → …
CitationsWeb of Science® Times Cited: 3
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 110737156