A framework for quantitative modeling and analysis of highly (re)configurable systems

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

*Corresponding author for this work

Research output: Contribution to journalJournal articlepeer-review

277 Downloads (Pure)


This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, like software product lines. Different combinations of the optional features of such systems give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. Our models are defined in the probabilistic feature-oriented language QFLan, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLan specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints and with a semantics based on discrete-time Markov chains. Our analysis is based on statistical model checking, which allow us to scale to larger models with respect to precise probabilistic techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost of specific system variants. Our approach is supported by a novel Eclipse-based tool including state-of-the-art DSL utilities for QFLan as well as analysis plug-ins. We provide a number of case studies that have driven and validated the development of our framework.
Original languageEnglish
JournalI E E E Transactions on Software Engineering
Issue number3
Pages (from-to)321 - 345
Publication statusPublished - 2020

Bibliographical note

See details of the publisher at https://ieeexplore.ieee.org/document/8405597/


  • Software product lines
  • Probabilistic modeling
  • Quantitative constraints
  • Statistical model checking
  • Formal methods


Dive into the research topics of 'A framework for quantitative modeling and analysis of highly (re)configurable systems'. Together they form a unique fingerprint.

Cite this