A Formal-Methods Approach to Provide Evidence in Automated-Driving Safety Cases

TL;DR

This paper demonstrates how formal methods can be used to generate compelling evidence for safety cases in automated driving, potentially reducing the need for extensive reviews and testing.

Contribution

It introduces a formal-methods-based approach to substantiate safety requirements and integrate them into safety cases for automated driving systems.

Findings

Formal methods can provide mathematical proofs of safety requirements.

Formal models can serve as requirements for system components.

Using formal proofs can reduce verification effort.

Abstract

The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to ensure correctness of automotive systems cannot explore the typically infinite set of possible behaviours. In contrast, formal methods are exhaustive methods that can provide mathematical proofs of correctness of models, and they can be used to prove that formalizations of functional safety requirements are fulfilled by formal models of system components. This paper shows how formal methods can provide evidence for the correct break-down of the functional safety requirements onto the components that are part of feedback loops, and how this evidence fits into the argument of the safety case. If a proof is obtained, the formal models are used as requirements on the components. This structure of the safety argumentation can be used to alleviate the need for reviews and tests to ensure that the break-down is correct, thereby saving effort both in data collection and verification time.