Statistical Model Checking for Product Lines

Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

339 Downloads (Pure)

Abstract

We report on the suitability of statistical model checking for the analysis of quantitative properties of product line models by an extended treatment of earlier work by the authors. The type of analysis that can be performed includes the likelihood of specific product behaviour, the expected average cost of products (in terms of the attributes of the products’ features) and the probability of features to be (un)installed at runtime. The product lines must be modelled in QFLan, which extends the probabilistic feature-oriented language PFLan with novel quantitative constraints among features and on behaviour and with advanced feature installation options. QFLan is a rich process-algebraic specification language whose operational behaviour interacts with a store of constraints, neatly separating product configuration from product behaviour. The resulting probabilistic configurations and probabilistic behaviour converge in a discrete-time Markov chain semantics, enabling the analysis of quantitative properties. Technically, a Maude implementation of QFLan, integrated with Microsoft’s SMT constraint solver Z3, is combined with the distributed statistical model checker MultiVeStA, developed by one of the authors. We illustrate the feasibility of our framework by applying it to a case study of a product line of bikes.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques : 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Number of pages20
Volume9952
PublisherSpringer
Publication date2016
Pages114-33
ISBN (Print)978-3-319-47165-5
ISBN (Electronic)978-3-319-47166-2
DOIs
Publication statusPublished - 2016
Event7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation - Corfu, Greece
Duration: 10 Oct 201614 Oct 2016
Conference number: 7

Conference

Conference7th International Symposium On Leveraging Applications Of Formal Methods, Verification And Validation
Number7
CountryGreece
CityCorfu
Period10/10/201614/10/2016
SeriesLecture Notes in Computer Science
ISSN0302-9743

Keywords

  • Software engineering techniques
  • Logics and meanings of programs
  • Programming languages, compilers, interpreters
  • Computation by abstract devices
  • Mathematical logic and formal languages
  • Artificial intelligence (incl. robotics)

Cite this

ter Beek, M. H., Legay, A., Lluch Lafuente, A., & Vandin, A. (2016). Statistical Model Checking for Product Lines. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I (Vol. 9952, pp. 114-33). Springer. Lecture Notes in Computer Science https://doi.org/10.1007/978-3-319-47166-2_8