A Formally Verified Highly Resilient Safety Concept with Degraded Modes for Automated Driving

Modern Automated Driving Systems (ADS) rely on fragmented safety measures to handle faults and make driving decisions. To eradicate lethal road accidents, safety engineering has to expand beyond contemporary automotive design practices and patterns. We present a holistic safety concept unifying advanced safety measures for handling multiple-point faults and fault-free hazardous situations associated with system performance limitations. Noteworthy, we illustrate how our safety mechanism mitigates triple-point faults, which are often beyond the focus of the safety community. Furthermore, on top of handling faults in the ADS, our design can effectively react to its own faults. To reduce specification errors, we developed an executable model of the safety concept in the formal specification language mCRL2. The behavior of the model is governed by a four-mode degradation policy controlling distributed processors, redundant communication networks, and virtual machines. To keep the vehicle as safe as possible our degradation policy can reduce driving comfort or ADS availability using additional low-cost driving channels. We formalized five safety requirements in the modal mu-calculus and proved them against our mCRL2 model, which is intractable to accomplish exhaustively using traditional road tests or simulation techniques. In conclusion, our formally proven safety concept defines a holistic design pattern for ADS minimizing road fatalities.