The challenges in providing convincing arguments for safe and correct
behavior of automated driving (AD) systems have so far hindered their
widespread commercial deployment. Conventional development approaches
such as testing and simulation are limited by non-exhaustive analysis,
and can thus not guarantee safety in all possible scenarios. Formal
methods can provide mathematical proofs that could be used to produce
rigorous evidence to support the safety argument. This paper investigates
the use of differential dynamic logic and the deductive verification tool
KeYmaera X in the development of an AD feature. Specifically, this paper
demonstrates how formal models and safety proofs of different design
variants of a Decision & Control module can be used in the safety
argument of an in-lane AD feature. In doing so, the assumptions and
invariant conditions necessary to guarantee safety are identified, and
the paper shows how such an analysis helps during the development process
in requirement refinement and formulation of the operational design
domain. Furthermore, it is shown how the performance of the different
models is formally analyzed exhaustively, in all their allowed behaviors.