Verification for Reliable Product Lines

TL;DR

This paper introduces a probabilistic model for verifying the reliability of product lines, comparing three techniques including a new bounded approach that efficiently verifies common behaviors across the entire product line.

Contribution

It proposes a feature-aware Markov chain model for product line reliability and introduces a novel bounded verification technique that improves efficiency over existing methods.

Findings

The bounded verification technique outperforms enumerative and parametric methods.

Experimental results show the advantages of the new bounded approach.

The model effectively captures probabilistic reliability properties of product lines.

Abstract

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.