Probability is an important component in the design and analysis of complex systems across a broad spectrum of application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, dynamic power management and biological systems. Probabilistic model checking is a formal verification technique for the modelling and analysis of such systems. It provides efficient and rigorous methods for evaluating a wide range of quantitative properties, from performance and reliability to security and anonymity.
Our work on probabilistic model checking involves:
- design and implementation of efficient tools and techniques, including the development of the state-of-the-art probabilistic model checker PRISM;
- development of the underlying formalisms, theory and algorithms, including for example abstraction techniques, process calculi and probabilistic timed automata;
- application of the techniques to real-world case studies, for example to the domains of ubiquitous and pervasive computing, to adaptive systems and to biological modelling.
