Verification of Variability-Intensive Stochastic Systems with Statistical Model Checking

Abstract

We propose a simulation-based approach to verify Variability-Intensive Systems (VISs) with stochastic behaviour. Given an LTL formula and a model of the VIS behaviour, our method estimates the probability for each variant to satisfy the formula. This allows us to learn the products of the VIS for which the probability stands above a certain threshold. To achieve this, our method samples VIS executions from all variants at once and keeps track of the occurrence probability of these executions in any given variant. The efficiency of this algorithm relies on Algebraic Decision Diagram (ADD), a dedicated data structure that enables orthogonal treatment of variability, stochasticity and property satisfaction. We implemented our approach as an extension of the ProVeLines model checker. Our experiments validate that our method can produce accurate estimations of the probability for the variants to satisfy the given properties.