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, with a recent shift towards synthesis from quantitative specifications. 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, the PRISM tool paper, 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 and synthesis
My work concentrates on formulating novel and powerful models, logics, algorithms, data structures and computational techniques to improve the efficiency of quantitative verification and synthesis techniques, and to further develop the probabilistic model checker PRISM. Main topics include model checking for probabilistic timed automata, quantitative software verification, as well as the more recent direction of quantitative runtime verification, see this CACM paper. We are also involved in the Predictable Software Systems project, part of LSCITS collaboration, described in this CACM paper.
The ESSLLI 2010 Summer School Tutorial on Probabilistic Model Checking serves as an overview of the field.
For recent work see the invited lecture on Automated Learning of Probabilistic Assumptions for Compositional Reasoning [PDF file] given at the 2011 ETAPS/FASE Conference, and the invited lecture 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). More detail can be found in two tutorial-style book chapters, on model checking for continuous time Markov chains and Markov decision processes.
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 collaborative/competitive stochastic protocols (see the PRISM-games extension) and medical medical devices, studied as part of the ERC Advanced Grant VERIWARE: From Software Verification to 'Everyware' Verification (see press release here), the Autonomous Ubiquitous Sensing project funded by Oxford Martin School, 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 paper Sensing Everywhere: Towards Safer and More Reliable Sensor-enabled Devices given at the SAFECOMP 2012 Conference, and 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).
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 at Birmingham). More recently, we have applied probabilistic model checking to DNA computation, see this paper (joint work with Luca Cardelli and Andrew Phillips at Microsoft, now supported by a Microsoft studentship).
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.