Verification for Reliable Product Lines
This work addresses reliability verification for critical product lines, presenting incremental improvements in verification efficiency.
The paper tackles the problem of verifying probabilistic properties, such as reliability, in product lines by proposing a model for feature-aware discrete-time Markov chains. It compares three verification techniques, finding that the parametric and new bounded techniques offer advantages over enumerative methods.
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.