Modelling and Model Checking Software Product Lines

Speaker

Andreas Classen (Uni Namur, B)
Title Modelling and Model Checking Software Product Lines
When 23.02.2011, 10:00
Where Room 5052
Abstract In product line engineering, systems are developed in families and
differences between family members are expressed in terms of features. We study the problem of model checking product line behaviours against temporal properties. This is more difficult than for single systems because a product line with n features yields up to 2^n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to have efficient formalisms and heuristics.

First, we propose featured transition systems, a semantic model that describes the combined behaviour of an entire system family. We then define a model checking algorithm that allows to verify featured transition systems against temporal properties. When it succeeds, all systems of the family satisfy the property. Otherwise, the algorithm pinpoints those that do not.

Second, we discuss two implementations of featured transition systems.
A first uses a symbolic representation of the state space and is implemented as part of the NuSMV model checker. The second, SNIP, uses a semi-symbolic on-the-fly algorithm.  SNIP comes with an intuitive specification language based on Promela. Benchmarks show that our algorithms outperform classical model checking algorithms executed over each system of the family separately.
Slides