Model Mining and Efficient Verification of Software Product Lines


  • Siavash Soleimanifard KTH Royal Institute of Technology Stockholm, Sweden
  • Dilian Gurov KTH Royal Institute of Technology Stockholm, Sweden
  • Ina Schaefer Technical University of Braunschweig Braunschweig, Germany
  • Bjarte M. Østvold Norwegian Computing Center Oslo, Norway
  • Minko Markov University of Sofia Sofia, Bulgaria



Product Families, Compositional Verification, Model Mining, Variability Models, Model Checking, Maximal Models


Software product line modeling aims at capturing a set of software products
in an economic yet meaningful way. We introduce a class of variability models
that capture the sharing between the software artifacts forming the products
of a software product line (SPL) in a hierarchical fashion, in terms of commonalities
and orthogonalities. Such models are useful when analyzing and verifying all products
of an SPL, since they provide a scheme for divide-and-conquer-style decomposition
of the analysis or  verification problem at hand. We define an abstract class of SPLs
for which variability models can be constructed that are optimal w.r.t. the chosen
representation of sharing.

We show how the constructed models can be fed into a previously developed
algorithmic technique for compositional verification of control-flow temporal safety
properties, so that the properties to be verified are iteratively decomposed into
simpler ones over orthogonal parts of the SPL, and are not re-verified over
the shared parts. We provide tool support for our technique, and evaluate
our tool on a small but realistic SPL of cash desks.