Probabilistic verification is a quantitative approach to verification of complex computer systems that has been the focus of intense research for over a decade. While in many circumstances of quantitative verification it is reasonable to anticipate a possible discrepancy between a stochastic model and the real-world system it represents, the state-of-the-art provides little account for the effects of this discrepancy on verification results. To address this problem, we present a perturbation approach in which quantities such as transition probabilities in the stochastic model are allowed to be perturbed from their measured values. We present a rigorous mathematical characterization for variations that can occur to verification results in the presence of perturbed quantities. The formal treatment is based on the analysis of a parametric variant of discrete-time Markov chains, called parametric Markov chains (PMCs), which are equipped with a metric to measure model perturbations. We employ an asymptotic method from perturbation theory to formulate and compute two groups of perturbation bounds, namely condition numbers and quadratic bounds, for verifying PMCs against !- regular properties. We also evaluate our approach with case studies on variant models for three widely studied systems, the Zeroconf protocol, the Leader Election Protocol and the NAND Multiplexer..
Paper Accepted at ICSE 2014