TY - JOUR
T1 - All roads lead to Rome
T2 - Commuting strategies for product-line reliability analysis
AU - Castro, Thiago
AU - Lanna, André
AU - Alves, Vander
AU - Teixeira, Leopoldo
AU - Apel, Sven
AU - Schobbens, Pierre Yves
N1 - Funding Information:
We thank the anonymous reviewers for the useful suggestions for improvement. This work was partially supported by the National Institute of Science and Technology for Software Engineering (INES) 9 9 , funded by CNPq [grant 465614/2014-0 ] and FACEPE [grant APQ-0388-1.03/14 ]. Thiago Castro acknowledges support from the Science and Technology Department of the Brazilian Army. Vander Alves would like to thank for the research grant CAPES ref. BEX 0557-16-1 / Alexander von Humboldt ref. 3.2-1190844-BRA-HFSTCAPES-E . Leopoldo Teixeira is supported by FACEPE [grant APQ-0570-1.03/14 ] and CNPq [grant 409335/2016-9 ]. Sven Apel is supported by the German Research Foundation ( AP 206/4 and AP 206/6 ).
Publisher Copyright:
© 2017 Elsevier B.V.
PY - 2018/1/15
Y1 - 2018/1/15
N2 - Software product line engineering is a means to systematically manage variability and commonality in software systems, enabling the automated synthesis of related programs (products) from a set of reusable assets. However, the number of products in a software product line may grow exponentially with the number of features, so it is practically infeasible to quality-check each of these products in isolation. There is a number of variability-aware approaches to product-line analysis that adapt single-product analysis techniques to cope with variability in an efficient way. Such approaches can be classified along three analysis dimensions (product-based, family-based, and feature-based), but, particularly in the context of reliability analysis, there is no theory comprising both (a) a formal specification of the three dimensions and resulting analysis strategies and (b) proof that such analyses are equivalent to one another. The lack of such a theory hinders formal reasoning on the relationship between the analysis dimensions and derived analysis techniques. We formalize seven approaches to reliability analysis of product lines, including the first instance of a feature-family-product-based analysis in the literature. We prove the formalized analysis strategies to be sound with respect to the probabilistic approach to reliability analysis of a single product. Furthermore, we present a commuting diagram of intermediate analysis steps, which relates different strategies and enables the reuse of soundness proofs between them.
AB - Software product line engineering is a means to systematically manage variability and commonality in software systems, enabling the automated synthesis of related programs (products) from a set of reusable assets. However, the number of products in a software product line may grow exponentially with the number of features, so it is practically infeasible to quality-check each of these products in isolation. There is a number of variability-aware approaches to product-line analysis that adapt single-product analysis techniques to cope with variability in an efficient way. Such approaches can be classified along three analysis dimensions (product-based, family-based, and feature-based), but, particularly in the context of reliability analysis, there is no theory comprising both (a) a formal specification of the three dimensions and resulting analysis strategies and (b) proof that such analyses are equivalent to one another. The lack of such a theory hinders formal reasoning on the relationship between the analysis dimensions and derived analysis techniques. We formalize seven approaches to reliability analysis of product lines, including the first instance of a feature-family-product-based analysis in the literature. We prove the formalized analysis strategies to be sound with respect to the probabilistic approach to reliability analysis of a single product. Furthermore, we present a commuting diagram of intermediate analysis steps, which relates different strategies and enables the reuse of soundness proofs between them.
KW - Model checking
KW - Product-line analysis
KW - Reliability analysis
KW - Software product lines
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85033214455&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2017.10.013
DO - 10.1016/j.scico.2017.10.013
M3 - Article
AN - SCOPUS:85033214455
SN - 0167-6423
VL - 152
SP - 116
EP - 160
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -