Source-linked AI summary
Correctness Guarantees for the Composition of Lane Keeping and Adaptive Cruise Control
Xiangru Xu, Jessy W. Grizzle, Paulo Tabuada, Aaron D. Ames
TL;DR
Simultaneously operating lane keeping and adaptive cruise control requires formal safety guarantees despite their interaction through vehicle dynamics. The paper combines contract-based modeling, control barrier functions, and quadratic programs to mediate safety and performance, yielding correct-by-construction control with a closed-form solution and CarSim simulation demonstration.
Problem
Formal correctness guarantees are more difficult for simultaneously operating safety or convenience modules because they are coupled through vehicle dynamics.
Method
The paper synthesizes CBFs using SOS optimization and physics-based modeling, then combines them with performance controllers in quadratic programs under assume-guarantee contracts.
Results
The resulting feedback control guarantees safety for the composed LK and ACC modules, and the quadratic-program solution is available in closed form.
Takeaways & Limitations
The framework can endow legacy performance controllers with correct-by-construction safety while allowing LK and ACC modules from different suppliers when contracts are provided.
Abstract
from arXiv · showhide
This paper develops a control approach with correctness guarantees for the simultaneous operation of lane keeping and adaptive cruise control. The safety specifications for these driver assistance modules are expressed in terms of set invariance. Control barrier functions are used to design a family of control solutions that guarantee the forward invariance of a set, which implies satisfaction of the safety specifications. The control barrier functions are synthesized through a combination of sum-of-squares program and physics-based modeling and optimization. A real-time quadratic program is posed to combine the control barrier functions with the performance-based controllers, which can be either expressed as control Lyapunov function conditions or as black-box legacy controllers. In both cases, the resulting feedback control guarantees the safety of the composed driver assistance modules in a formally correct manner. Importantly, the quadratic program admits a closed-form solution that can be easily implemented. The effectiveness of the control approach is demonstrated by simulations in the industry-standard vehicle simulator Carsim.
I. INTRODUCTION
The paper addresses the challenge of guaranteeing safety when lane keeping and adaptive cruise control operate simultaneously through coupled vehicle dynamics. It proposes a modular, correct-by-construction framework based on contracts, control barrier functions, and quadratic programming.
- Motivation: LK maintains lane position through active steering, while ACC regulates speed or following distance using comfort-based acceleration bounds.ACC’s specification is treated as a safety constraint despite its legal classification as a convenience feature.
- Motivation: Simultaneous operation of coupled driver-assistance modules makes formal correctness guarantees more challenging than for individual systems.The paper frames LK and ACC composition as a coupled-system verification problem.
- Approach: Control barrier functions encode safety through invariant sets, while quadratic programs combine barrier conditions with performance controllers.The barrier formulation avoids computing reachable sets directly and ensures forward invariance when admissible controls satisfy the CBF condition.
- Approach: The proposed approach uses assume-guarantee contracts to capture interactions between LK and ACC through vehicle and environment dynamics.The contracts consist of subsystem assumptions and guarantees.
- Contribution: The framework supports individual or simultaneous LK and ACC activation and is demonstrated through calculations and simulation on a mid-size passenger-vehicle model.The paper describes LK with a continuous-time linear system and ACC with a linear parameter-varying system.
III. PROBLEM FORMULATION
The paper formulates the composition problem by introducing separate LK and ACC models and safety specifications, then defining an assume-guarantee contract between the modules.
- III. PROBLEM FORMULATION: The section introduces the individual models and specifications for LK and ACC before formulating their composition problem.The contract specifies assumptions and guarantees used to relate the two subsystems.
A. Dynamic Models
The dynamic models represent LK through lateral-yaw vehicle motion and ACC through longitudinal point-mass dynamics, with bounded inputs and disturbances reflecting vehicle operation and comfort constraints.
- A. Dynamic Models: LK uses a lateral-yaw model, while ACC uses a point-mass model for longitudinal vehicle dynamics.The two models are introduced as the basis for the LK and ACC specifications.
- A. Dynamic Models: The LK state contains lateral displacement, lateral velocity, yaw-angle deviation, and yaw rate, with front-wheel steering as input.The desired yaw rate is computed from road curvature and longitudinal vehicle velocity.
- A. Dynamic Models: The ACC state contains the following-car speed, lead-car speed, and intervehicle distance, with wheel force as input.The model also accounts for aerodynamic drag and lead-vehicle acceleration.
- A. Dynamic Models: The LK steering angle and ACC acceleration/deceleration are bounded to reflect admissible vehicle inputs and driver comfort.Comfort-based acceleration limits are substantially below the vehicle’s maximum deceleration capability.
- A. Dynamic Models: The lead and controlled vehicles may have different allowable deceleration capabilities, so their acceleration bounds need not be equal.This distinction is included in the ACC modeling assumptions.
B. Specifications
The paper separates LK and ACC requirements into hard safety constraints and soft performance objectives. LK constrains lane position and related states, while ACC constrains following distance and pursues driver-selected speed when compatible with safety.
- Hard constraints must hold for all time, whereas soft performance objectives may be overridden when they conflict with safety.
- LK Specifications: LK requires the absolute lateral displacement |y| to remain below the lane-dependent bound ym.The bound reflects the lane width and vehicle dimensions.
- LK Specifications: LK additionally bounds lateral velocity, yaw-angle deviation, and yaw rate, while optionally limiting lateral acceleration to respect driver comfort.The example comfort bound is |ν̇| ≤ 0.25g, and yaw-rate tracking of the road’s turning rate is a soft objective.
- ACC Specifications: ACC requires the controlled vehicle to maintain a safe distance from the lead car using a minimum-distance and desired-time-headway formulation.The desired time headway is τd, and D0 denotes the minimum stopped-car distance.
- ACC Specifications: ACC also aims to reach a driver-selected desired speed, but this objective cannot be achieved when the lead car travels more slowly.The formulation handles this conflict without explicit if-then-else operating modes.
C. Formulating the Composition Problem
The composition problem seeks feedback controllers that preserve LK and ACC safety constraints under disturbances and bounded inputs while achieving soft objectives whenever they do not conflict with safety. The challenge is that lateral and longitudinal dynamics are coupled through vehicle speed and lateral-yaw terms.
- The paper seeks feedback controllers for LK and ACC that always satisfy hard constraints under admissible d and aL, while achieving soft constraints when compatible with safety.
- LK and ACC interact because the lateral model depends on longitudinal speed, while longitudinal dynamics include a lateral-velocity–yaw-rate product.External inputs d and aL, together with bounded control inputs, further complicate composition.
- Figure 3 depicts the interconnection between the vehicle’s lateral and longitudinal dynamics.
D. A Contract Between LK and ACC
The paper uses a contract between LK and ACC to separate controller design while preserving composition-level safety. Each subsystem assumes a bound supplied by the other and guarantees its own coupling-variable bound or safe state set.
- The contract-based approach specifies assume-guarantee relations between LK and ACC using bounds on their respective coupling variables.
- LK assumes bounded controlled-vehicle speed and guarantees its state remains in XLK for every admissible desired yaw rate d.
- ACC assumes a bound on the product of lateral velocity and yaw rate and guarantees controlled-vehicle speed remains in Dvf for every admissible lead-car acceleration.
- Respecting the individual contracts permits separate LK and ACC controller design while preserving all compositional safety constraints.The paper constructs individual CBFs and then combines them with performance controllers through a QP.
IV. CONTROL BARRIER FUNCTIONS FOR LK AND ACC
The paper constructs control barrier functions for LK and ACC by translating their hard constraints into conditions that ensure forward-safe closed-loop trajectories. This section introduces the CBF construction for both models.
- CBFs are provided for the LK and ACC models by converting hard specifications into conditions that guarantee the safety portion of those specifications.
A. The CBF For LK
The LK control barrier function is synthesized as a polynomial whose certified set is nonempty, remains within the modeled operating bounds, and is controlled invariant under admissible steering. Sum-of-squares programs and an iterative volume-maximization procedure construct and refine this certificate.
- CBF properties: The polynomial h_lk is designed to make C_lk nonempty, preserve LK state bounds, and satisfy the CBF condition over allowed speeds and desired yaw rates.These properties imply the LK hard constraints and guarantee an admissible steering angle that keeps trajectories in C_lk when initialized there.
- SOS synthesis: Theorem 3 gives sufficient polynomial and SOS conditions for constructing h_lk with the certified region D set to X_LK.The construction uses polynomial multipliers and constraints over state, speed, and desired-yaw-rate domains.
- SOS synthesis: The synthesis normalizes the polynomial coefficients and maximizes κ to enlarge the volume of the controlled-invariant set C_lk.Normalization prevents coefficient scaling from artificially increasing κ.
- Iterative refinement: If the initialization program P0 is feasible, Algorithm 1 terminates and returns a polynomial satisfying LK-P1 through LK-P3.The initialization uses an LQR gain and scales the controller so the steering input remains within U_lk.
- Design interpretation: The constructed controller is not implemented directly; the CBF instead characterizes a safe set that later control inputs can render controlled invariant.This separates certificate construction from the eventual feedback law and avoids requiring the SOS-search controller itself to be deployed.
- Iterative refinement: The iterative procedure alternates controller and CBF construction, with each iteration producing a set no smaller than the previous one and guaranteeing asymptotic convergence.The next controller-search step remains feasible after the CBF-update step; termination occurs by a κ-change threshold or a preset iteration count.
B. The CBF For ACC
The ACC barrier function is designed to enforce the contract’s following-distance and invariance requirements while accounting for vehicle dynamics. A physics-based deceleration bound corrects the conservatism introduced by direct SOS construction.
- CBF construction: The ACC CBF h_acc is designed to satisfy the contract-defined properties governing safe following distance and controlled invariance.The candidate barrier uses a polynomial ĥ_acc(v_f, v_l) whose properties are specified by the ACC contract.
- Safety guarantee: The CBF-certified set implies a minimum safe distance D_min = τ_dv_f + D_0 + ĥ_acc(v_f, v_l), which is at least τ_dv_f + D_0.This ensures the hard following-distance constraint when the ACC state lies in C_acc.
- Physics-based refinement: Direct SOS construction produced an unnecessarily large D_min, motivating physics-based optimization that exploits the ACC subsystem’s monotone property.The paper identifies conservatism as undesirable because it can encourage other vehicles to cut into the lane.
- Physics-based refinement: The deceleration bound accounts for aerodynamic drag and the contract’s bound on ν_r when constructing the ACC barrier function.The resulting closed-form CBFs satisfy ACC-P1 through ACC-P3.
V. COMPOSITIONAL CONTROL SYNTHESIS VIA QUADRATIC PROGRAM
The compositional controller combines CBF-based safety constraints with performance objectives through separate quadratic programs for LK and ACC. The resulting feedback law preserves the hard constraints while permitting nominal or legacy controllers to be overridden when necessary.
- QP formulation: The QPs encode CBF conditions as hard safety constraints and nominal-controller objectives as soft constraints that yield when safety conflicts with performance.This prioritizes lane keeping and following-distance specifications over closeness to a performance controller.
- Composition: The contract makes the compositional controlled-invariant set the Cartesian product C_lk × C_acc, allowing LK and ACC controllers to be synthesized through separate QPs.Decoupling holds while each subsystem state remains within its respective certified set.
- QP formulation: LK performance is represented through a nominal LQR-based controller, while ACC performance uses a CLF condition with relaxation variable δ2 and convergence parameter c.The QP formulation also permits penalized relaxation variables for soft constraints.
- Implementation: The convex QPs can be solved efficiently, and their controls also admit locally Lipschitz closed-form solutions suitable for embedded implementation.The closed-form solutions are obtained by computing minimum distances to convex sets.
- Guarantee: The generated controls constitute a locally Lipschitz feedback law that satisfies the LK and ACC hard constraints for all time.Additional performance objectives, such as lateral-acceleration bounds, can be added as soft constraints without losing hard-constraint satisfaction.
VI. SIMULATION
The LK and ACC controllers were evaluated simultaneously in Carsim using QP-based control laws designed from simplified vehicle models. The simulation kept the stated safety constraints satisfied while tracking speed and lane-related performance objectives.
- Simulation setup: The controllers were applied simultaneously to LK and ACC in a 16-degree-of-freedom Carsim vehicle model.The controllers were designed using simplified continuous-time models, while the overall simulated system satisfied the safety specifications.
- Simulation setup: The simulation used a D-Class Sedan with a 0.25 g maximum deceleration, 0.06 rad maximum steering angle, desired speed vd = 22 m/s, and desired time headway τd = 1.8 seconds.The lateral bounds included ymax = 0.9 m, νmax = 1 m/s, ∆ψmax = 0.05 rad, and rmax = 0.3 rad/s.
- Controller design: CBFs were constructed using SOS optimization for LK, while ACC used optimal barriers; QPs were solved numerically and admit closed-form implementation.The LK feedback gain was obtained from an LQR problem with the specified preview, state-weight, and control-weight choices.
- Longitudinal behavior: The controlled car accelerated toward the desired speed, slowed to maintain safe distance, and later matched the lead car’s speed without if-then-else mode logic.The QP enforced hard safety constraints while meeting the soft speed-tracking objective as closely as possible.
- Safety constraints: The lateral states stayed within their bounds despite road-curvature steps, while wheel force and steering angle remained within their specified limits.The reported wheel-force and steering-angle constraints were satisfied throughout the simulation.
- Safety and performance: The yaw-rate reference was tracked, actual time headway stayed at least as large as desired, and both hacc and hlk remained positive.Positive hacc implied satisfaction of the ACC constraint, while positive hlk implied satisfaction of the LK constraints.
VII. CONCLUSIONS
The paper concludes that QP-based control barrier function feedback can provide correctness guarantees for simultaneous lane keeping and adaptive cruise control. The framework supports modular controllers and can be implemented with a closed-form QP solution, while full-sized-vehicle validation and model and sensor-error assessment remain future challenges.
- Conclusions: The approach enforces LK and ACC safety constraints as hard CBF conditions while treating performance objectives as soft constraints.The resulting longitudinal force and steering angle are generated by quadratic programs.
- Conclusions: The framework can integrate legacy performance controllers and provide correct-by-construction safety guarantees for simultaneously activated modules.The QP solution can be implemented without online optimization because it is known in closed form.
- Modularity: Assume-guarantee contracts allow independently supplied LK and ACC modules to operate safely together when an OEM provides the correct contracts.The paper presents this contract structure as suited to modular driver-assistance systems.
- Limitations and future work: The evaluation reported here is simulation-based, with only preliminary tests on the Khepera robot and Robotarium testbed.Future work includes full-sized-vehicle testing, model validation, and accounting for sensor errors when constructing CBFs.