Professor Marta Kwiatkowska is happy to supervise projects in the area of probabilistic modelling and verification, particularly those relating to the PRISM model checker. PRISM is an open source formal verification tool for analysis of probabilistic systems. PRISM has an extensive website which includes software for download, tutorial, manual, publications and many case studies.
One possibility is to undertake a modelling and verification case study in PRISM. Example application domains are:
- randomised communication and multimedia protocols
- probabilistic security protocols
- biological process modelling
- randomised distributed algorithms
See the "Case Studies" section of the PRISM website for more information, including already developed models and verification results.
Secondly, there are various opportunities to enhance or improve the functionality of the PRISM model checker itself. Examples include:
- development of a framework for using external input languages in PRISM, e.g. SBML, process algebras
- investigation of efficient binary decision diagram (BDD) heuristics for PRISM models
- implementation of arbitrary precision engines for PRISM to enable the solution of linear equation systems and linear optimisation problems
- overhaul of the (currently very basic) text-based editor for PRISM models
- implementation of a new property editor for PRISM, including a translator from English specifications to temporal logic
- development of a graphical modelling language for PRISM
