Model Mining and Efficient Verification of Software Product Lines

Soleimanifard, Siavash, et al. "Model Mining and Efficient Verification of Software Product Lines." Serdica Journal of Computing 9.1 (2015): 35-82. <http://eudml.org/doc/281455>.

@article{Soleimanifard2015,
abstract = {Software product line modeling aims at capturing a set of software products in an economic yet meaningful way. We introduce a class of variability models that capture the sharing between the software artifacts forming the products of a software product line (SPL) in a hierarchical fashion, in terms of commonalities and orthogonalities. Such models are useful when analyzing and verifying all products of an SPL, since they provide a scheme for divide-and-conquer-style decomposition of the analysis or verification problem at hand. We define an abstract class of SPLs for which variability models can be constructed that are optimal w.r.t. the chosen representation of sharing. We show how the constructed models can be fed into a previously developed algorithmic technique for compositional verification of control-flow temporal safety properties, so that the properties to be verified are iteratively decomposed into simpler ones over orthogonal parts of the SPL, and are not re-verified over the shared parts. We provide tool support for our technique, and evaluate our tool on a small but realistic SPL of cash desks.},
author = {Soleimanifard, Siavash, Gurov, Dilian, Schaefer, Ina, Østvold, Bjarte, Markov, Minko},
journal = {Serdica Journal of Computing},
keywords = {Product Families; Compositional Verification; Model Mining; Variability Models; Model Checking; Maximal Models},
language = {eng},
number = {1},
pages = {35-82},
publisher = {Institute of Mathematics and Informatics Bulgarian Academy of Sciences},
title = {Model Mining and Efficient Verification of Software Product Lines},
url = {http://eudml.org/doc/281455},
volume = {9},
year = {2015},
}

TY - JOUR
AU - Soleimanifard, Siavash
AU - Gurov, Dilian
AU - Schaefer, Ina
AU - Østvold, Bjarte
AU - Markov, Minko
TI - Model Mining and Efficient Verification of Software Product Lines
JO - Serdica Journal of Computing
PY - 2015
PB - Institute of Mathematics and Informatics Bulgarian Academy of Sciences
VL - 9
IS - 1
SP - 35
EP - 82
AB - Software product line modeling aims at capturing a set of software products in an economic yet meaningful way. We introduce a class of variability models that capture the sharing between the software artifacts forming the products of a software product line (SPL) in a hierarchical fashion, in terms of commonalities and orthogonalities. Such models are useful when analyzing and verifying all products of an SPL, since they provide a scheme for divide-and-conquer-style decomposition of the analysis or verification problem at hand. We define an abstract class of SPLs for which variability models can be constructed that are optimal w.r.t. the chosen representation of sharing. We show how the constructed models can be fed into a previously developed algorithmic technique for compositional verification of control-flow temporal safety properties, so that the properties to be verified are iteratively decomposed into simpler ones over orthogonal parts of the SPL, and are not re-verified over the shared parts. We provide tool support for our technique, and evaluate our tool on a small but realistic SPL of cash desks.
LA - eng
KW - Product Families; Compositional Verification; Model Mining; Variability Models; Model Checking; Maximal Models
UR - http://eudml.org/doc/281455
ER -