Skip to main content
Thesis defences

PhD Oral Exam - Oumaima Barhoumi, Electrical and Computer Engineering

Formally Verified Barrier Certificates for Car-Following Traffic Safety


Date & time
Tuesday, December 1, 2026
9 a.m. – 12 p.m.
Format

In-person

Cost

This event is free

Organization

School of Graduate Studies

Contact

Dolly Grewal

Where

Engineering, Computer Science and Visual Arts Integrated Complex
1515 Ste-Catherine St. W.
Room 1.162

Accessible location

Yes - See details

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

Automated driving is changing how vehicles perceive traffic, make decisions, and regulate their motion. Connected and automated vehicles (CAVs) combine automated control with information obtained from onboard sensors, other vehicles, or infrastructure. Their operation becomes more difficult in mixed traffic, where automated and human-driven vehicles share the road without necessarily exchanging information or following the same decision processes. Under these conditions, safety depends not only on the behavior of an individual CAV, but also on how its actions affect and are affected by the surrounding traffic.

This thesis defines explicit safety conditions for longitudinal interactions and develops controllers intended to preserve them. The considered safety constraints metrics include Time-To-Collision (TTC), which characterizes closing urgency between a follower and its leader, and Time Headway (THW) describing the available spacing relative to the follower's speed. A TTC requirement is expressed as a barrier certificate, which defines the boundary between safe and unsafe interaction states. Its evolution under longitudinal vehicle dynamics then yields a control barrier condition, a bounded acceleration controller, and an explicit feasibility criterion. Subsequently, we propose a combined TTC-THW control barrier function (CBF), a method that converts a safety specification into control-input constraints, to cover closing, non-closing, and equal-speed interactions. Higher-order control barrier functions further extend CBFs, by differentiating the safety condition until acceleration appears, to represent fixed and adaptive spacing-error envelopes. Throughout this development, feasibility is assessed against the available acceleration limits.

We formalize the safety definitions, barrier interpretations, control conditions, and feasibility results in the Lean 4 theorem prover and machine-check their proofs. The TTC and TTC--THW proofs concern states and inputs satisfying their assumptions, whereas the spacing-based development includes conditional trajectory-preservation results under stronger assumptions. Traffic simulation using the CARLA driving simulator and recorded highway trajectories provide complementary evidence about the implemented controllers.

In the evaluated cases, the controllers produce feasible bounded actions where the stated conditions hold, remove the observed short-TTC and THW-threshold violations in selected highway interactions, and support the regulation of fixed and adaptive spacing envelopes. The thesis therefore provides a structured basis for assessing longitudinal CAV interactions under explicit models, assumptions, and control limits without making an unconditional claim about deployment safety.