University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Marta Kwiatkowska - Research Overview

Computing infrastructure has become indispensable in our society, with examples ranging from online banking, to intelligent vehicles and electronic medical equipment. Software faults in such systems can have disastrous consequences. My research is concerned with developing modelling and automated verification techniques that can guarantee the stable, safe, secure, timely, reliable and resource-efficient operation of computing systems. Model checking is a verification technique that can establish whether certain properties, usually expressed in temporal logic, hold for a system model. The models describe how systems move between states by executing actions, and are typically represented as state-transition graphs. Model checking explores all system executions and, unlike testing, amounts to a mathematical proof. This task is inherently challenging in view of infinite state spaces and undecidability of the underlying problem. In conventional model checking, the properties of interest are qualitative, such as safety (e.g. "the car will never stall while driving autonomously" for intelligent vehicles).

The distinctive aspect of my work is its focus on probabilistic and quantitative verification techniques, with a recent shift towards synthesis from quantitative specifications. I led the development of the internationally leading probabilistic symbolic model checker PRISM, which has been applied to several real-world case studies, with unusual behaviour discovered in some of these. PRISM systematically explores a model of a system against properties such as "what is the worst case time to deliver an update from the sensor monitoring distance to the car ahead?" (for an intelligent vehicle) and "what is the expected power consumption during the first hour of operation?" (in a body-sensor network). ore 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. PRISM proved its usefulness in exceptionally many distinct fields, including distributed and cloud computing, wireless networks, security, robotics, quantum computing, game theory, biology and nanotechnology.


Research themes

My research can be roughly grouped into the following themes: