Counterexample Guided Abstraction Refinement of product-line behavioural models

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

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 apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments 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. We discuss in which cases a given abstraction should be used.

Original languageEnglish
Title of host publication22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Proceedings
PublisherACM Press
Pages190-201
Number of pages12
Volume16-21-November-2014
ISBN (Electronic)9781450330565
DOIs
Publication statusPublished - 16 Nov 2014
Event22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014 - Hong Kong, China
Duration: 16 Nov 201421 Nov 2014

Conference

Conference22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE 2014
Country/TerritoryChina
CityHong Kong
Period16/11/1421/11/14

Keywords

  • Abstraction
  • CEGAR
  • Model checking
  • Software product lines

Fingerprint

Dive into the research topics of 'Counterexample Guided Abstraction Refinement of product-line behavioural models'. Together they form a unique fingerprint.

Cite this