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.