AbstractsEngineering

Annually over 60.000 people die and another 3.7 million get injured in car accidents in the United States and Europe combined. Automation of vehicles can reduce the number of accidents by 90%. Therefore, it is of great interest in academia and industry. For the automated vehicles that are being presented in industry however, proofs of safe performance are generally not found. Therefore, this thesis investigates approaches to automatically assess automated vehicle controller performance such as deviation overshoot and obtained lateral speeds. More specifically, this thesis studies so-called formal verification of the performance of a highway lane change controller. Because of its robustness properties, a Sliding Mode Control (SMC) strategy is selected and in this research several variations are designed. The availability of a lower level controller was assumed to generate the required steering torque, which results in a third order linear vehicle model. Nonlinear vehicle models with higher order dynamics were considered as well but showed to be too complex for the verification approach. Due to the switching nature of SMC, the closed loop system is modelled as a Hybrid System and as such verified using multiple verification packages. The abstraction based environment HSolver can provide full formal guarantees that account for intervals of parameter uncertainty, in this case initial deviation and lateral speed. However, in comparison with simulations using the Matlab Toolbox Breach–which only propagates distinct values and cannot provide formal guarantees for entire intervals–it suffers from a large over-approximation. Still, for a limited initial interval, HSolver analyses show that a SMC variant called Quasi Sliding Mode Control (QSMC) results in a safe lane change in terms of deviation overshoot. More advanced controllers show promising performance in Breach simulations. This suggests that techniques to reduce the over-approximation in HSolver, or developments in similar tools, can be very interesting to verify safety for more general situations in future research. Alternatively, other performance criteria or different parametric uncertainties could be formally verified as well.