Verification for Reliable Product Lines
Maxime Cordy, Patrick Heymans, Pierre-Yves Schobbens, Amir, Molzam Sharifloo, Carlo Ghezzi, Axel Legay

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Software Engineering Methodologies · Flexible and Reconfigurable Manufacturing Systems · Safety Systems Engineering in Autonomy
