Abstract. We demonstrate how probabilistic model checking, a formal verification method for the analysis of systems which exhibit stochastic behaviour, can be applied to the study of dependability properties of software-based control systems. We provide an overview of these techniques and of the probabilistic model checking tool PRISM, illustrating the usefulness of the approach through a small case study. By using existing formalisms and tool support, we show how it is possible to construct large and complex Markov models from an intuitive high-level description. Furthermore, we are able to take advantage of the efficient implementation techniques which have been developed for these tools.