Variability-Specific Abstraction Refinement for Family-Based Model Checking

Aleksandar Dimovski, Andrzej Wasowski

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationFundamental 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
EditorsMarieke Huisman, Julia Rubin
Number of pages17
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Publication date23 Mar 2017
Pages406-423
ChapterFASE 2017
ISBN (Print)978-3-662-54493-8
ISBN (Electronic)978-3-662-54494-5
DOIs
Publication statusPublished - 23 Mar 2017
EventFundamental 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, Sweden
Duration: 22 Apr 201729 Apr 2017
http://www.etaps.org/

Conference

ConferenceFundamental 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
LocationUppsala University
Country/TerritorySweden
CityUppsala
Period22/04/201729/04/2017
Internet address
SeriesLecture Notes in Computer Science
Volume10202
ISSN0302-9743

Keywords

  • Family-Based Model Checking
  • Abstraction and Partition Refinement
  • fLTL properties

Fingerprint

Dive into the research topics of 'Variability-Specific Abstraction Refinement for Family-Based Model Checking'. Together they form a unique fingerprint.

Cite this