Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles

We combine theorem proving and reachability analysis for cyber-physical systems verification to arrive at a practical approach to safe waypoint-following for an autonomous mobile vehicle controlled by a learning-enabled controller. We propose a robust monitor verifying short-term and long-term safety simultaneously at runtime, thereby combining the benefits of both theorem proving and reachability analysis. The proposed novel monitor architecture allows temporary violation of long-term safety while maintaining short-term safety to recover to a state with long-term safety. The recovery is based on a fallback model predictive controller. The experiments conducted in a high-fidelity racing car simulator demonstrate that our framework is safe and resilient in path tracking scenarios, in which avoiding collision with the race track boundary and obstacles is required.