2013/11/06 by Maxime Cordy, Patrick Heymans, Cordy, Maxime +9
Computer Science · Engineering · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Flexible and Reconfigurable Manufacturing Systems #Safety Systems Engineering in Autonomy #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1311.1343
openalex publication_date 2013/11/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.