Variability-Specific Abstraction Refinement for Family-Based Model Checking

Aleksandar Dimovski, Andrzej Wasowski

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

Variational systems are ubiquitous in many application areas today. They use features to control presence and absence of system functionality. One challenge in the development of variational systems is their formal analysis and verification. Researchers have addressed this problem by designing aggregate so-called family-based verification algorithms. Family-based model checking allows simultaneous verification of all variants of a system family (variational system) in a single run by exploiting the commonalities between the variants. Yet, the computational cost of family-based model checking still greatly depends on the number of variants. In order to make it computationally cheaper, we can use variability abstractions for deriving abstract family-based model checking, where the variational model of a system family is replaced with an abstract (smaller) version of it which preserves the satisfaction of LTL properties. The variability abstractions can be combined with different partitionings of the set of variants to infer various verification scenarios for the variational model. However, manually finding an optimal verification scenario is hard since it requires a good knowledge of the family and property, while the number of possible scenarios is very large.

In this work, we present an automatic iterative abstraction refinement procedure for family-based model checking. We use Craig interpolation to refine abstract variational models based on the obtained spurious counterexamples (traces). The refinement procedure works until a genuine counterexample is found or the property satisfaction is shown for all variants in the family. We illustrate the practicality of this approach for several variational benchmark models.
OriginalsprogEngelsk
TitelFundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 : Fundamental Approaches to Software Engineering, FASE 2017
RedaktørerMarieke Huisman, Julia Rubin
Antal sider17
UdgivelsesstedBerlin, Heidelberg
ForlagSpringer
Publikationsdato23 mar. 2017
Sider406-423
KapitelFASE 2017
ISBN (Trykt)978-3-662-54493-8
ISBN (Elektronisk)978-3-662-54494-5
DOI
StatusUdgivet - 23 mar. 2017
BegivenhedFundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017: Fundamental Approaches to Software Engineering, FASE 2017 - Uppsala University, Uppsala, Sverige
Varighed: 22 apr. 201729 apr. 2017
http://www.etaps.org/

Konference

KonferenceFundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
LokationUppsala University
Land/OmrådeSverige
ByUppsala
Periode22/04/201729/04/2017
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind10202
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Variability-Specific Abstraction Refinement for Family-Based Model Checking'. Sammen danner de et unikt fingeraftryk.

Citationsformater