Families of dependable systems:a model checking approach

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 lectures, 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 productsof the family, visualise the family/products behaviour and efficiently model check properties expressed in MHML over products and families alike. The use of the above methods, techniques and tools will be applied to a scenario derived from a family of dependable systems.