Safe and Protected: Combining Protection Mechanism with Safety Verification In Autonomous Vehicles

Protection mechanisms, also known as security mechanisms, in automotive systems are proactive components that continuously monitor vehicle signals to detect early signs of potential faults. For autonomous vehicles, it is essential that safety models, such as Responsibility-Sensitive Safety (RSS), which governs longitudinal and lateral safety, account for these mechanisms to enable timely and effective countermeasures against imminent actuation failures. A typical example is the proactive application of braking to increase longitudinal distance and mitigate the risk of losing braking capability. In this paper, we present a data-centric approach for modeling protection mechanisms using the SmartData framework, which facilitates the automatic derivation of safety properties for real-time formal verification via a Safety Enforcement Unit (SEU). We introduce extensions to RSS proper response strategies, enabling them to anticipate potential actuation constraints by leveraging shared internal states of protection mechanisms and a predictive time-to-trigger metric. We formally demonstrate that our approach preserves compliance with the original RSS safety guarantees by extending its inductive proof structure. Furthermore, we validate the feasibility of our solution through empirical evaluation, showing that the embedded formal verification can automatically extract properties from publish-subscribe message systems and operate at runtime with minimal overhead (less than 1% of platform processing capacity). Finally, we integrate our approach with RSS and a representative protection mechanism within the CARLA simulator to showcase its effectiveness in a realistic autonomous driving environment.