Analysis of probabilistic models of Software Product Lines with Quantitative Constraints using MultiVeStA


QFLan is a probabilistic feature-oriented language to specify models of software product lines with probabilistic configurations and behaviour, e.g. by considering a QFLan semantics based on discrete-time Markov chains. Quantitative constraints can affect products generated by QFLan models, like “bikes can have a certain maximum price and weight”, “bikes without an engine can weigh at most 10 kg” or “only bikes costing more than 250 euros can be sold”.

A prototypal Maude implementation of QFLan exists, combined with the state-of-the-art Microsoft’s SMT solver Z3.

The QFLan interpreter has been combined with the distributed statistical model checker MultiVeStA to perform quantitative analyses of software product lines.


QFLan and its integration with Z3 and MultiVeStA is discussed in detail in the following two papers:

In both publications, the tool has been used to analyse a bikes product line. The presented analyses include the likelihood of certain behaviour of interest (e.g. disposal of broken bike), the expected average cost and weight of bikes, and the probability of install and uninstall certain features.


A ready to use version of MultiVeStA integrating QFLan is available here together with all files necessary to reproduce the experiments discussed in the two publications.


For suggestions, remarks, bugs or requests please do not hesitate to contact any of us (in alphabetical order):

  • maurice.terbeek@isti.cnr.it
  • albl@dtu.dk
  • andrea.vandin@imtlucca.it


Research supported by EU project QUANTICOL (600708) and Italian MIUR project CINA (PRIN 2010LHT4KM).

We thank Dorel Lucanu, Grigore Rosu, Andrei Stefanescu, and Andrei Arusoaie for sharing with us their own integration of Maude and z3, which we adapted for our purposes.