Reliability Modelling of Disk Subsystems with Probabilistic Model Checking

Abstract

We discuss how probabilistic model checking, a variant of model checking, can be useful in modelling multiple failures in disk subsystems, as it allows specification of probabilities or rates of transitions also. Probabilistic model checking can be used to not only check the correctness of formulae that are augmented with a probability operator, but also to compute, as a side effect, probabilities and Markov rewards in response to queries expressed in an expressive logic. With exponential distributions for failures, it is possible to accurately compute the reliability of many non-trivial disk systems. Exploiting the technique of symmetry reduction, it is possible to handle even larger fully symmetric systems. For non-exponential distributions, such as Weibull models of disk reliability, we can analyze reasonable sized systems (such as RAID4/5/6) if good approximations based on exponomials are possible. We report our experiences and compare our results with those from simulation.