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 [21, 27], 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 [24] and I developed and implemented a run-time verification system for the management of domestic wireless networks [25]. 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 [19].

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 [4, 5, 6, 8]. Our end goal is to achieve security and resilience by design for future vehicular systems. Our industrial partners are NXP and Blue Bear.

UAV

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 [14] 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 [21] 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 [18] for more details. This is joint work with Prof McCann at Imperial College and her group.

Bigraphical model of example sensor network

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 [16, 23]. This research is in collaboration with the System Control Design Group at NATS, the main air navigation service provider in the UK.

Air traffic radar

Awards/Grants

  1. Amazon Research Award: Automated Reasoning
    From Whiteboards to Models: Diagrammatic Formal Modelling for Everyone, 2022 - 2023.
  2. PETRAS National Centre of Excellence for IoT Systems Cybersecurity
    FARM: Formal methods for Agritech Resilience Modelling, 2021 - 2022.
  3. PETRAS National Centre of Excellence for IoT Systems Cybersecurity
    FARM: Formal methods for Agritech Resilience Modelling, 2021 - 2022.
  4. EPSRC Impact Acceleration Account
    HEVMAX: Formal models for xEV range maximisation, 2021.
  5. PETRAS National Centre of Excellence for IoT Systems Cybersecurity
    MAGIC: Multi-Perspective Design of IoT Cybersecurity in Ground and Aerial Vehicles, 2020 - 2022.
  6. The Royal Society International Exchanges Cost Share 2019 MOST Taiwan
    Digital twins for monitoring, optimisation, and automation in Agritech, 2020 - 2022.
  7. The Royal Society of Edinburgh International Exchange Programme: RSE - MOST Joint Project
    Formal methods for Internet of Things (IoT) device management platforms, 2017 - 2018.
  8. SICSA (Scottish Informatics and Computer Science Alliance) - PECE Bursary
    Collaboration with Prof Mortier on the definition of formal approaches based on bigraphs to model analyse and automatically deploy IoT and Cloud systems, 2015 - 2016.
  9. London Mathematical Society - Computer Science Small Grant
    Funded to visit Prof Haverkort at the University of Twente (Netherlands). The aim of the visit was to study stochastic processes in the context of Bigraphical Reactive Systems and safety critical systems, November 2014.
  10. The Royal Society - International Exchange Scheme and
    SICSA (Scottish Informatics and Computer Science Alliance) - PECE Bursary
    Funded to start a collaboration with Prof Sengupta at UC Berkeley aimed at defining new frameworks for modelling and analysis of heterogeneous mobile robotic systems based on the theory of bigraphs, October 2013.