Augmenting Formal Models with Transport Data to Support Digital Twinning for Transport Decarbonisation
Supervisor: Dr Ricardo Almeida
School: Computing Science
Description:
This project offers an opportunity for a student to contribute to TransiT: Digital Twinning for Transport Decarbonisation (https://transit.ac.uk/), a major UK research programme developing next-generation digital twin technologies to support the decarbonisation of transport systems. TransiT brings together leading universities, policymakers, and a wide range of industrial stakeholders across logistics and transport, including major freight operators, infrastructure providers, and technology companies. The programme works with large-scale, real-world datasets, such as long-haul and airport logistics data from DHL, road fleet operations from Tesco, and last-mile delivery route data from UPS.
Project Overview
The student will work at the intersection of formal modelling and practical transport systems. The project centres on bigraphs, introduced by Robin Milner, as a mathematical framework for modelling dynamic, distributed systems. Informally, bigraphs provide a unified way to represent both spatial structure (for example, vehicles within depots, depots within regions) and connectivity structure (such as routing, communication, and resource flows).
The project will use the BigraphER tool, which supports modelling and analysis of bigraphical reactive systems, enabling simulation, verification, and exploration of system behaviour, allowing formal reasoning about complex operational scenarios. BigraphER has been developed at the University of Glasgow (https://www.dcs.gla.ac.uk/~michele/bigrapher.html), and its main developers are also contributing investigators of TransiT.
Research Context
The theory of bigraphs is currently being extended to support data-aware modelling, allowing structured data to be stored and manipulated directly within the formal framework. The student will help evaluate and shape these developments by:
- assessing how the extended framework performs on real transport datasets
- identifying modelling challenges arising in practice
- providing structured feedback to inform refinements of both the theory and the tooling
- developing small case studies demonstrating the integration of data-rich transport scenarios within BigraphER.
Student Activities
The student will:
- learn the fundamentals of bigraph theory
- gain experience with the BigraphER tool
- explore selected datasets from transport partners
- construct formal models of transport scenarios
- evaluate the expressiveness and limitations of current extensions.
Skills
The project is suited to a student with:
- strong mathematical interest
- curiosity about formal methods, sustainability, and complex systems.
While BigraphER is implemented in OCaml, no prior knowledge of OCaml is required.
Expected Outcomes
By the end of the internship, the student will have:
- gained research experience in formal methods
- worked with industrial-scale data
- contributed to tools supporting transport decarbonisation.