[KNP04c] Marta Kwiatkowska, Gethin Norman and David Parker. Controller Dependability Analysis By Probabilistic Model Checking. In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04), pages 177-182, Elsevier. April 2004. [ps.gz] [pdf] [bib] [Illustrates the applicability of probabilistic model checking and PRISM to analysing dependability properties for a simple model of a software-based control systems.]
Downloads:  ps.gz ps.gz (258 KB)  pdf pdf (705 KB)  bib bib
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.