Verification of Probabilistic Real-time Systems

This talk will give an introduction to probabilistic model checking, a formal verification technique for systems that exhibit stochastic behaviour. These methods have been used to analyse a wide range of systems, including communication protocols, such as Bluetooth and FireWire, randomised security protocols, e.g. for anonymity and contract signing, and many others. This talk will give an overview of the basic theory and techniques for a probabilistic model checking, with a particular focus on systems that incorporate real-time behaviour. It will also illustrate the applicability of these methods using a selection of real-world case studies that have been verified with the probabilistic model checker PRISM.