Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2016 P-252, 79-80 (2016).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Counterexample guided abstraction refinement of product-line behavioural models

Maxim Cordy , Patrick Heymans , Axel Legay , Pierre-Yves Schobbens , Bruno Dawagne and Martin Leucker


The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we recall the main ideas of a paper published elsewhere that applies CEGAR (Counterexample-Guided Abstraction Refinement) and desings new forms of abstraction specifically for SPLs. Experiments are carried out to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-646-6

Last changed 25.02.2016 18:39:08