ITU

Efficient family-based model checking via variability abstractions

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

Standard

Efficient family-based model checking via variability abstractions. / Dimovski, Aleksandar; Al-Sibahi, Ahmad Salim; Brabrand, Claus; Wasowski, Andrzej.

In: International Journal on Software Tools for Technology Transfer, Vol. 19, No. 5, 26.05.2016, p. 585–603.

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

Harvard

APA

Vancouver

Author

Bibtex

@article{70588a4a8f3a476a9c6f45566468b1df,
title = "Efficient family-based model checking via variability abstractions",
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.",
keywords = "Family-Based Model Checking, Abstract Interpretation, Feature Transition System",
author = "Aleksandar Dimovski and Al-Sibahi, {Ahmad Salim} and Claus Brabrand and Andrzej Wasowski",
year = "2016",
month = may,
day = "26",
doi = "10.1007/s10009-016-0425-2",
language = "English",
volume = "19",
pages = "585–603",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer",
number = "5",

}

RIS

TY - JOUR

T1 - Efficient family-based model checking via variability abstractions

AU - Dimovski, Aleksandar

AU - Al-Sibahi, Ahmad Salim

AU - Brabrand, Claus

AU - Wasowski, Andrzej

PY - 2016/5/26

Y1 - 2016/5/26

N2 - 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.

AB - 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.

KW - Family-Based Model Checking

KW - Abstract Interpretation

KW - Feature Transition System

U2 - 10.1007/s10009-016-0425-2

DO - 10.1007/s10009-016-0425-2

M3 - Journal article

VL - 19

SP - 585

EP - 603

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 5

ER -

ID: 81558913