Andreas Classen (Uni Namur, B)
|Title||Modelling and Model Checking Software Product Lines|
|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.
- Subscribe to the ics feed.
- No Events