Introduction
Autonomous vehicles (AVs) sit at the centre of the AI for Transportation and Logistics theme's own example applications
These applications including: intelligent intersection management for connected and autonomous vehicles, ride-sharing and dynamic bus routing, micro-tolling to reduce congestion, personalised EV charging and routing, and digital-twin fleet and shipping-route optimisation. Each is an AI system whose entire justification is sustainability; reduced energy and resource use, more efficient smart mobility services, less congestion.
These benefits, however, are only realised while the system keeps operating as designed. When conditions depart from what was anticipated at design time, a degraded sensor, an unfamiliar road layout, an extreme weather event, an AV or routing system typically falls back to conservative behaviour: harder braking, longer or more cautious routes, reduced platooning, disabled dynamic pricing, or handover to a human operator. These fallback behaviours are safe, but they are also resource-inefficient, and they erode the very energy, congestion and emissions gains the system was deployed to deliver. Current verification methods check behaviour against a fixed set of predefined scenarios; they give no mathematical guarantee about what happens to safety, trust, or sustainability performance once a system is pushed outside that envelope.
Primary Research Question:
How can formal methods mathematically prove that autonomous vehicle systems remain safe and trusted, and continue to deliver bounded environmental benefit, when operating conditions diverge from those anticipated at design time?
RQ1: Safety and Trust Baseline Formalisation: Before resilience can be verified, there must be a precise baseline to verify it against. How can existing AV safety standards be formalised into mathematically verifiable properties (e.g. "the vehicle must maintain a following distance of at least 3 seconds", "emergency braking must engage within 0.5 seconds of obstacle detection"), together with corresponding trust properties (consistency of behaviour, transparency of decision explanations), so both can serve as a shared baseline for resilience verification? These trust properties will be identified partly through video-elicited reflection sessions with users [7], surfacing what transparency and consistency actually mean to them in practice, rather than assuming it from safety standards alone.
RQ2: Resilience Verification Under Environmental and Operational Uncertainty: Given the RQ1 baseline, how can formal refinement and model checking prove that safety and trust properties are preserved, or degrade in a bounded, predictable way, under conditions not anticipated during design, such as sensor degradation, extreme weather, or unfamiliar traffic patterns?
RQ3: Sustainability-Bounded Resilience: Fallback behaviours that preserve safety are not cost free: excess braking, rerouting and cautious driving all carry an energy and emissions penalty. Can formal methods bound this penalty, proving not only that a fallback behaviour is safe, but that its environmental cost stays within a defined limit, so resilience verification becomes a certificate of sustained environmental benefit, not only sustained safety?
The Gap:
Existing resilience research in autonomous transport [1, 2] treats fallback and degraded mode behaviour as a safety concern, with its energy and emissions cost largely unexamined. No existing formal verification method proves bounds on the environmental cost of a system's own safety mechanisms. Connecting formal resilience verification directly to the environmental case for AV deployment, rather than treating sustainability as a separate framing layer, is the project's central novel contribution.
Research Approach
The project is organised in three phases. RQ1 provides the minimum formal foundation required; RQ2 and RQ3 form the substantive core of the PhD and are where the majority of research time is spent.
Phase 1: Baseline Formalisation: systematic analysis of existing AV safety standards and trust literature [e.g. 3, 4, 5], formalised into a shared formal model of safety and trust properties. This phase is deliberately scoped to reach a working baseline quickly so the project's weight sits on resilience, not on rederiving safety models from scratch.
Phase 2: Resilience Verification (core phase): model the perturbations an AV or connected mobility system may encounter, sensor faults, extreme weather, unfamiliar traffic patterns, using formal refinement [6], and prove that the Phase 1 safety and trust properties either hold or degrade within mathematically defined bounds. Case studies target the theme's own example applications directly, e.g. proving that an intelligent intersection controller for connected and autonomous vehicles, or a dynamically routed ride-share/bus fleet, remains provably safe when a subset of sensor or connectivity inputs becomes unreliable.
Phase 3: Sustainability-Bounded Resilience (core phase, overlapping with Phase 2): extend the resilience models to treat energy/emissions cost as a first-class verified quantity, proving upper bounds on the resource penalty of fallback behaviour. Case studies draw directly on the theme's named applications, personalised EV charging and routing under sensor uncertainty, digital-twin fleet and shipping-route optimisation under unusual traffic patterns, and micro-tolling schemes that must keep reducing congestion even when demand or sensing conditions are unexpected, to keep the formal models grounded in scenarios central to the theme's sustainability mission.
Throughout, the research uses Event-B [6] formal method for systematic, incremental model development and model checking for automated verification, building on established formal methods practice for safety-critical systems.
References:
1. Hoppe I, Hagemann W, Stierand I, Hahn A, Bolles A. Challenges for trustworthy autonomous vehicles: Let us learn from life. Systems Engineering. 2024;27:789–800. https://doi.org/10.1002/sys.21744 (2024)
2. Johnsen, Stig Ole et al. A Review of Resilience in Autonomous Transport to Improve Safety and Security. Proceedings of the 30th European Safety and Reliability Conference and 15th Probabilistic Safety Assessment and Management Conference (2020)
3. Asieh Salehi Fathabadi and Pauline Leonard. "Trust equals less death - it's as simple as that" : Developing a Socio-technical Framework for Trustworthy Defence and Security Automated Systems. In Proceedings of the Second International Symposium on Trustworthy Autonomous Systems (TAS '24). https://doi.org/10.1145/3686038.3686071 (2024)
4. Michael Akintunde, Victoria Young, Vahid Yazdanpanah, Asieh Salehi Fathabadi, Pauline Leonard, Michael Butler, and Luc Moreau. Verifiably Safe and Trusted Human-AI Systems: A Socio-technical Perspective. In Proceedings of the First International Symposium on Trustworthy Autonomous Systems (TAS '23). https://doi.org/10.1145/3597512.3599719 (2023)
5. Asieh Salehi Fathabadi and Vahid Yazdanpanah. Trust modelling and verification using Event-B. Fifth Workshop on Formal Methods for Autonomous Systems. doi:10.4204/EPTCS.395.2 (2023)
6. Abrial, J.R. Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
7. Nora McIntyre, Andri Christodoulou and Anthony Onwuegbuzie. Come to re-think of it: complementary approaches to own-perspective videos for prompting teacher cognitions in controversy-rich science education. ESERA. (2025)