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

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

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.

langue originaleAnglais
titreSoftware Engineering 2016
Sous-titreFachtagung des GI-Fachbereichs Softwaretechnik : 23-26 Februar 2016 Wien
rédacteurs en chefJens Knoop, Uwe Zdun
EditeurGesellschaft fur Informatik (GI)
Pages79-80
Nombre de pages2
ISBN (Electronique)9783885796466
Etat de la publicationPublié - 2016
EvénementSoftware Engineering-Konferenz, SE 2016 - Software Engineering Conference, SE 2016 - Wien, Autriche
Durée: 23 févr. 201626 févr. 2016

Série de publications

NomLectures Notes in Informatics
EditeurGesellschaft für Informatik
VolumeP-252
ISSN (imprimé)1617-5468

Une conférence

Une conférenceSoftware Engineering-Konferenz, SE 2016 - Software Engineering Conference, SE 2016
PaysAutriche
La villeWien
période23/02/1626/02/16

Empreinte digitale

Examiner les sujets de recherche de « A primer on counterexample guided abstraction refinement of product-line behavioural models ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation