Marta Kwiatkowska - Research Overview
My research is mainly concerned with modelling and analysis methods for concurrent systems, and particularly analysis through automatic verification (aka model checking). My work spans the whole spectrum, from theory (process calculi, semantic models, logics, algorithms) to implementation techniques (symbolic/SAT methods, abstraction/refinement, numerical solutions, software verification) and applications (wireless communication and security protocols, randomised distributed coordination, asynchronous hardware).
The main focus of my research over the past several years has been on quantitative verification of systems, and specifically probabilistic model checking techniques. We have developed the internationally leading probabilistic model checker PRISM, which has been applied to several real-world case studies, with unusual behaviour discovered in some of these. More information is available from the PRISM website and this book.
Probability plays a very important role in modelling and functioning of complex systems: it is used as a symmetry breaker in distributed coordination algorithms, and for analysing performance and Quality of Service properties. Stochastic process calculi and the corresponding verification and analysis methods are being used to describe and reason about wireless networks, security protocols and biological organisms.
Research themes
My research can be roughly grouped into the following themes:
- Quantitative probabilistic model checking
My work concentrates on formulating novel and powerful models, logics, algorithms, data structures and computational techniques to improve the efficiency of quantitative verification techniques, and to further develop the probabilistic model checker PRISM. Main topics include model checking for probabilistic timed automata and automated verification for probabilistic mobile calculi, as well as the more recent direction of quantitative software verification, the subject of the recently completed project Automated quantitative software verification with PRISM. We are also involved in the Predictable Software Systems project, part of LSCITS collaboration.
The ESSLLI 2010 Summer School Tutorial on Probabilistic Model Checking serves as an overview of the field.
See also the invited paper on Advances and Challenges of Probabilistic Model Checking [PDF file] given at the 48th Annual Allerton Conference on Communication, Control and Computing, October 2010, the invited paper on Quantitative Verification: Models, Techniques and Tools [Slides, PDF file] given at the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), and this book chapter.
The International Conference on Quantitative Evaluation of SysTems (QEST) is the main conference in the area.
-
Modelling and verification for ubiquitous computing
This theme is centred on applications of probabilistic model checking, mainly using the PRISM toolset, to model and analyse ubiquitous computing systems. Earlier work involved analysing the performance of wireless protocols, security protocols and embedded systems, for example Bluetooth and IEEE 802.15.4 Zigbee. Current research is addressing quantitative software verification for ubiquitous computing systems, see the ERC Advanced Grant VERIWARE: From Software Verification to 'Everyware' Verification (see press release here), the recently completed project UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures, and the foundations and verification of components and connectors, studied as part of the CONNECT-IP: Emergent Connectors for Eternal Software Intensive Networked Systems Framework 7 EU project.
See my invited lecture A Framework for Verification of Software with Time and Probabilities [PDF file], given at the 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), and invited lecture On quantitative software verification [Slides, PDF file], given at the SPIN 2009 Workshop on Model Checking of Software.
See also the Ubiquitous Computing (UbicompGC) Grand Challenge manifesto at this link.
- Computational modelling and analysis of biological systems
This theme aims to apply techniques developed in computer science, such as process calculi and model checking, to model biological biological systems. Thus derived models can be used to obtain new quantitative predictions in silico, which can guide the design and selection of in vitro experiments. We have applied stochastic pi-calculus and the PRISM model checker to model and analyse signalling pathways and cellular crypt structures. See the completed project Predictive modelling of signalling pathways via probabilistic model checking with PRISM (joint with John Heath).
See my lecture Simulation and verification for computational modelling of signalling pathways [Slides, PDF file] given at the Algorithmic Bioprocesses conference, and this Top Cited paper.
For general motivation see also this paper in the Journal of Cell Science and a mention of my work in Nature, see the online version or as it appeared in print.