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

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

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 2016
PublisherGesellschaft fur Informatik (GI)
Pages79-80
Number of pages2
VolumeP252
ISBN (Electronic)9783885796466
Publication statusPublished - 2016
EventSoftware Engineering-Konferenz, SE 2016 - Software Engineering Conference, SE 2016 - Wien, Austria
Duration: 23 Feb 201626 Feb 2016

Conference

ConferenceSoftware Engineering-Konferenz, SE 2016 - Software Engineering Conference, SE 2016
CountryAustria
CityWien
Period23/02/1626/02/16

Keywords

  • Abstraction
  • Cegar
  • Model checking
  • Software product lines

Fingerprint 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