David Parker
Professor of Computer Science, University of Birmingham
[Par13] David Parker. Verification of Probabilistic Real-time Systems. In Proc. 2013 Real-time Systems Summer School (ETR'13). August 2013. [pdf] [A short overview of probabilistic model checking for probabilistic real-time systems.]
Downloads:  pdf pdf (275 KB)
Abstract. Probabilistic model checking is a formal verification technique for systems that exhibit stochastic behaviour. It has 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 paper gives a short introduction to probabilistic model checking, with a particular focus on systems that incorporate real-time behaviour. We describe the model of probabilistic timed automata (PTAs), which can be used to represent systems with both probabilistic and real-time characteristics. We illustrate how to formally specify quantitative properties of PTAs, and give a brief summary of the techniques and tools that can be used to verify them. Pointers are provided throughout to further reading on this and related topics.