Modeling and Verification for Probabilistic Properties in Software Product Lines

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.