Efficient family-based model checking via variability abstractions

Aleksandar Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, Andrzej Wasowski

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

Many software systems are variational: they can be configured to meet diverse sets of requirements. They can produce a (potentially huge) number of related systems, known as products or variants, by systematically reusing common parts. For variational models (variational systems or families of related systems),
specialized family-based model checking algorithms allow efficient verification of multiple variants, simultaneously, in a single run. These algorithms, implemented in a tool Snip, scale much better than ``the brute force'' approach, where all individual systems are verified using a single-system model checker, one-by-one. Nevertheless, their computational cost still greatly depends on the number of features and variants. For variational models with a large number of features and variants, the family-based model checking may be too costly or even infeasible.

In this work, we address two key problems of family-based model checking. First, we improve scalability by introducing abstractions that simplify variability. Second, we reduce the burden of maintaining specialized family-based model checkers, by showing how the presented variability abstractions can be used to model check variational models using the standard version of (single-system) Spin. The variability abstractions are first defined as Galois connections on semantic domains. We then show how to use them for defining abstract family-based model checking, where a variability model is replaced with an abstract version of it, which preserves the satisfaction of LTL properties. Moreover, given an abstraction, we define a syntactic source-to-source transformation on high-level modelling languages that describe variational models, such that the model checking of the transformed high-level variational model coincides with the abstract model checking of the concrete high-level variational model. This allows the use of Spin with all its accumulated optimizations for efficient verification of variational models without any knowledge about variability. We have implemented the transformations in a prototype tool, and we illustrate the practicality of this method on several case studies.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume19
Issue number5
Pages (from-to)585–603
Number of pages19
ISSN1433-2779
DOIs
Publication statusPublished - 26 May 2016

Keywords

  • Family-Based Model Checking
  • Abstract Interpretation
  • Feature Transition System

Fingerprint

Dive into the research topics of 'Efficient family-based model checking via variability abstractions'. Together they form a unique fingerprint.

Cite this