About the project
The aim of this project is to explore how mathematical modelling and verification techniques (formal methods) can be used to prove that autonomous vehicle systems are safe, trustworthy, and resilient.
Autonomous vehicles (AVs) have the potential to transform future mobility by reducing congestion, lowering emissions, and supporting sustainable transport. However, safety and public trust remain significant barriers to widespread adoption. Current verification techniques provide limited assurance of safe behaviour, while models of trust in automation lack formal, mathematical grounding. This project aims to bridge these gaps through a multidisciplinary integration of computer science, formal verification, and social science to develop mathematically proven models of safety, trust, and resilience in autonomous vehicle systems.
The research will focus on three interconnected themes:
- safety verification will establish mathematically verifiable safety properties derived from existing standards and operational requirements, for example, ensuring vehicles maintain safe following distances or respond within specific timeframes to detected obstacles. These formal safety models will provide a foundation for the next phase of the work
- trust verification will extend formal methods to model and verify how user trust evolves in response to system behaviour, transparency, and reliability, capturing, for instance, how consistent decision-making or clear communication of vehicle intentions can enhance user confidence and long-term acceptance
- resilience verification will develop models to prove that AV systems maintain safe and trustworthy performance under uncertainty, such as novel traffic patterns or extreme weather, beyond those anticipated during design
You will:
- develop mathematical models of safety, trust, and resilience using the Event-B formal method and ProB model checking
- analyse current AV safety standards to identify gaps and formalise verifiable safety properties
- create and evaluate new formal models that link system behaviour to user trust and acceptance
- contribute to advancing assurance frameworks for intelligent and autonomous transport systems
The project will suit candidates interested in formal methods, autonomous systems, and human–AI interaction.
