Many product lines are critical, and therefore reliability is a vital part of their requirements. Reliability is a probabilistic property. We therefore propose a model for feature-aware discrete-time Markov chains as a basis for verifying probabilistic properties of product lines, including reliability. We compare three verification techniques: The enumerative technique uses PRISM, a state-of-the-art symbolic probabilistic model checker, on each product. The parametric technique exploits our recent advances in parametric model checking. Finally, we propose a new bounded technique that performs a single bounded verification for the whole product line, and thus takes advantage of the common behaviours of the product line. Experimental results confirm the advantages of the last two techniques.
@article{arxiv.1311.1343,
title = {Verification for Reliable Product Lines},
author = {Maxime Cordy and Patrick Heymans and Pierre-Yves Schobbens and Amir Molzam Sharifloo and Carlo Ghezzi and Axel Legay},
journal= {arXiv preprint arXiv:1311.1343},
year = {2013}
}