Research

My research lies on the boundaries between mathematics (logics, category theory, probability) and computer science (event-based systems, formal methods, model checking, process calculi). On this page you can find a brief description of my main research themes.

Theory

In my Ph.D. I extended the theory of bigraphs to bigraphs with sharing [6, 12]: a mathematical model for representing the spatial configuration of physical or virtual objects, which may include 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 [9] and I developed and implemented a run-time verification system for the management of domestic wireless networks [10]. 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 [4].

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 my current projects.

Mixed-reality systems

I recently developed a general bigraphical 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 [5] for more details. I am further focussing on this research area as part of the activities related to the SICSA Research Challenge on Next Generation Mixed-Reality Systems of which I am the leader.

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 prior to their deployment and at runtime. Refer to [1] for more details. This is joint work with Prof McCann at Imperial College and her group.

Bigraphical model of example
	     sensor network

IoT & DevOps

The aim of this strand of research is to develop tools and (formal) techniques based on bigraphs to assist operations staff to write, maintain and debug configuration files for IoT and Cloud systems. This will involve developing new methods to make bigraphical approaches more user-friendly and more expressive to facilitate the modelling process and, at the same time, more efficient with respect to performing complex analysis tasks. I collaborate on this with Dr Mortier at the University of Cambridge and Prof Yi-Bing Lin at the National Chiao Tung University (Taiwan).

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 [3, 8]. 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

Autonomous vehicles & swarm

I am working on developing new frameworks for modelling, analysing and controlling systems of autonomous vehicles. This involves extensions of the theory of bigraphs in several ways, to make it more expressive, and more suitable for an efficient implementation. In particular, this involves a notion of distance in the spatial model of bigraphs to model quantitative aspects of GPS sensing. The formal model allows us to check invariants to promptly flag warnings when they are not satisfied. Moreover, it is possible to optimise the management of limited resources such as the usage of an expensive satellite data link or power consumption. This research is in collaboration with Dr Pereira at UC Berkeley [7] and Prof Kontis at the School of Engineering of the University of Glasgow.

UAV

Awards/Grants

  1. The Royal Society of Edinburgh International Exchange Programme: RSE - MOST Joint Project
    Formal methods for Internet of Things (IoT) device management platforms, 2017 - 2018.
  2. SICSA (Scottish Informatics and Computer Science Alliance) - Research Challenge
    Next Generation Mixed-Reality Systems, 2016 - 2017.
  3. SICSA (Scottish Informatics and Computer Science Alliance) - PECE Bursary
    Collaboration with Dr Mortier on the definition of formal approaches based on bigraphs to model analyse and automatically deploy IoT and Cloud systems, 2015 - 2016.
  4. 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.
  5. 2nd Heidelberg Laureate Forum
    Selected for 100 spaces available for each discipline of mathematics and computer science, September 2014.
  6. 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.
  7. Marktoberdorf Summer School
    Logics and Languages for Reliability and Security, August 2009.