A primer on counterexample guided abstraction refinement of product-line behavioural models

Maxime Cordy, Bruno Dawagne, Patrick Heymans, Axel Legay, Martin Leucker, Pierre Yves Schobbens


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.

Original languageEnglish
Title of host publicationSoftware Engineering-Konferenz, SE 2016
Number of pages2
PublisherGesellschaft für Informatik e.V.
Publication date2016
ISBN (Print)978-388579646-6
Publication statusPublished - 2016
EventSoftware Engineering-Konferenz, SE 2016 - Software Engineering Conference - Wien, Austria
Duration: 23.02.201626.02.2016


Dive into the research topics of 'A primer on counterexample guided abstraction refinement of product-line behavioural models'. Together they form a unique fingerprint.

Cite this