Title of talk: Modelling, analysing and verifying variability by means of Modal Transition Systems


Our aim is a unifying logical framework for modelling, analysing and verifying behavioural variability. We use Modal Transition Systems for modelling the behaviour and a suitable branching-time temporal logic interpreted over MTSs for the necessary additional constraints. Our tool accepts a product family specified as a MTS, possibly with additional variability constraints, after which it can be used for the derivation and analysis of the family's products, as well as for the efficient verification of properties (over products and families alike) through model checking.