[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.]
|
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.
|