We propose an emerging solution technique and a support tool for
modelling and analysing variability in product families.
First we illustrate how to manage variability in a formal
framework consisting of a Modal Transition System (MTS) and an
associated set of formulae expressed in the variability and
action-based branching-time temporal logic vaCTL.
We then introduce the tool VMC, which accepts as input the
specification of a product family in a CCS-like process algebra,
possibly with an additional set of variability constraints. We
show how VMC can be used to automatically generate all valid
products of this family, defined in the same process algebra, as
well as to visualise the family (products) as modal (labelled)
transition systems. Finally, we show how VMC can efficiently
verify functional properties expressed as formulae in vaCTL,
over products and families alike, by means of its on-the-fly
model-checking algorithm.
This is joint work with FMT members Patrizia Asirelli, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, and Aldi Sulova