A number of models, logics and associated tools for the qualitative analysis of variability aspects and their use to deal with adaptability and evolvability of systems have recently been proposed. In these notes, we will introduce the action-based branching-time temporal logic MHML which allows expressing constraints over the products of a family as well as constraints over their behaviour in a single logical framework. Based on model-checking techniques for MHML, a modelling and verification framework will be presented that can automatically generate all the valid products of the family, visualise the family/products behaviour and efficiently model check properties expressed in MHML over products and families alike.