Research
My research is within the field of formal modelling and verification with a particular focus on spatial and probabilistic aspects. On this page, you can find a brief description of my main research themes.
Theory
My main contribution to date is bigraphs with sharing [27, 33], a mathematical model for representing the spatial configuration of physical or virtual objects, including overlapping spatial regions, and their interaction capabilities. I applied this to aspects of the hidden node problem in the 802.11 wireless communication protocol with RTS/CTS exchange [30] and I developed and implemented a run-time verification system for the management of domestic wireless networks [31]. The latter involved working closely with engineers (as part of the EPSRC Homework project) to develop a production system implemented on a router, as well as the reasoning environment for bigraphs BigraphER [25].
Applications
My research hypotheses are validated by routinely working side-by-side with other research groups and industry stakeholders to deploy, use and test my mathematical techniques in-the-wild. Below is a list of current application areas.
Cybersecurity in connected and autonomous vehicles
The widespread adoption of connected and autnomous vehicles is critically dependent on them being reliable, safe, secure, and resilient, especially when humans are in the loop. However, current engineering practice cannot provide guarantees that these properties are met at all times when a vehicle is operating. The consequence is that potential issues remain unforeseen during the design phase of these systems only to later emerge after deployment, often with tragic consequences. The research activities within the MAGIC project aim at tackling the limitations of current approaches by introducing a new modelling and verification paradigm based on online digital twins and multiple design perspectives each one encompassing a property of concern. Some preliminary results are in [10, 11, 12, 14]. Our end goal is to achieve security and resilience by design for future vehicular systems. Our industrial partners are NXP and Blue Bear.
IoT
This strand of research aims to develop tools and (formal) techniques based on bigraphs to assist operations staff to write, maintain and debug IoT systems. This will involve developing new methods and tools [20] to make bigraphical approaches more user-friendly and more expressive to facilitate the modelling process and, at the same time, more efficient to perform complex analysis tasks. I collaborate on this with Prof Lin and Dr Shieh at the National Chiao Tung University (Taiwan).
Mixed-reality systems
I recently developed a general bigraph model capable of representing physical and virtual space, human users, mobile and wearable sensors and devices, their interactions (human/human, human/machine and machine/machine) and GPS signal (including ghosting and drifting); how to solve the problems of recognition of virtual regions (and behaviours on the region borders) starting from the detected physical position of the users; how to fit the model with user trials. Refer to [26] for more details. I am further focussing on this research area as part of the SOCIAL CDT with the PhD project Optimising Interactions with Virtual Environments.
Multitenancy in large-scale sensor networks
Recent technological advancements and growing demand are driving the development of Wireless Sensor Networks towards supporting shared sensing infrastructures. For example, in applications such as those found in Smart Cities, multiple tenants are required to operate over the sensing infrastructure, sharing resources while achieving their individual goals. However, this paradigm shift raises important issues, such as ensuring the requirements of applications are met while sharing network resources, and preventing the depletion of resources leading to the rapid decrease of the network lifetime or utility. The goal of our research is to define a systematic approach to ensuring that requirements of resource-competing applications are satisfied by a target sensor network both before their deployment and at runtime. Refer to [23] for more details. This is joint work with Prof McCann at Imperial College and her group.
Reliability in navigational air service infrastructure
I am interested in investigating how predictive event-based modelling can inform operational decision making in complex systems with component failures. By relating the status of components to service availability, and using stochastic temporal logic reasoning, it is possible to quantify the risk of service failure now, and in the future, after a given elapsed time. Decisions can then be taken according to those risks. The chosen model can be calibrated according to inferences over historical field data, thus the results of the reasoning can inform decision making in the actual deployed system. An example of this approach is described in [22, 29]. This research is in collaboration with the System Control Design Group at NATS, the main air navigation service provider in the UK.
