Modeling and Verification for Probabilistic Properties in Software Product Lines
Abstract
Abstract—We propose a model for feature-aware discrete-time Markov chains, called FDTMC, as a basis for verifying probabilistic properties, e.g., reliability and availability, of product lines. To verify such properties on FDTMC, we compare three techniques. First, we experiment with two different parametric techniques to obtain this formula: the classical one builds it from the model as whole, and a new one that builds it compositionally from a sequence of modules. Finally, we propose a new technique that performs a bounded verification for the whole product line, and thus takes advantage of the high probability of common behaviors of the product line. It computes an approximate formula, represented as an arithmetic decision diagram. Experimental results on a vital signal monitoring system prototype are provided and compared for these techniques aiming at analysing them for scalability issues of size and computational time. They show complementary advantages, and we provide criteria to choose a technique depending on the characteristics of the model.
BibTex references
@inproceedings{DBLP:conf/hase/RodriguesANLCSS15,
author = {Gena{\'{\i}}na Nunes Rodrigues and
Vander Alves and
Vinicius Nunes and
Andr{\'{e}} Lanna and
Maxime Cordy and
Pierre{-}Yves Schobbens and
Amir Molzam Sharifloo and
Axel Legay},
title = {Modeling and Verification for Probabilistic Properties in Software
Product Lines},
booktitle = {16th {IEEE} International Symposium on High Assurance Systems Engineering,
{HASE} 2015, Daytona Beach, FL, USA, January 8-10, 2015},
pages = {173--180},
year = {2015},
crossref = {DBLP:conf/hase/2015},
url = {http://dx.doi.org/10.1109/HASE.2015.34},
doi = {10.1109/HASE.2015.34},
timestamp = {Fri, 29 Apr 2016 12:29:01 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/hase/RodriguesANLCSS15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/hase/2015,
title = {16th {IEEE} International Symposium on High Assurance Systems Engineering,
{HASE} 2015, Daytona Beach, FL, USA, January 8-10, 2015},
publisher = {{IEEE} Computer Society},
year = {2015},
url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7027113},
isbn = {978-1-4799-8110-6},
timestamp = {Tue, 16 Jun 2015 19:31:28 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/hase/2015},
bibsource = {dblp computer science bibliography, http://dblp.org}
}