Abstract. PRISM is a probabilistic model checker which allows the modelling and analysis of systems that exhibit probabilistic behaviour. Such tools have been developed to allow the analysis of specifications which require performance and reliability measures, as well as correctness.

The project described in this dissertation adds to the functionality of PRISM by providing a simulator - a tool which calculates and reasons about execution paths through probabilistic models. The first part of the project was to design and implement a simulator user interface, allowing users to manually or automatically generate and visualise execution paths through their models. This user interface has already been used extensively by members of the PRISM development team to debug their PRISM models and to help other users with their problems. Feedback from such users indicate that the PRISM simulator is very useful as a debugger of PRISM models and specifications, but also as a means of understanding the behaviour of models and even the behaviour of PRISM itself.

The second part of the project was to investigate and develop efficient algorithms which use statistical sampling techniques to perform approximate model checking of temporal logic specifications. The solution allows the user to specify the degree of approximation and the amount of confidence to which they require their results. One of the key motivations for these techniques is that they do not need to enumerate the entire state space, and thus can handle larger models. The success of these techniques is demonstrated by their application to models that are much larger than what PRISM can currently handle on a standard PC and by a comparison of their results to what can be calculated by PRISM.