  A fail-operational system for highly automated driving must complete the
driving task even in the presence of a failure. This requires redundant
architectures and a mechanism to reconfigure the system in case of a failure.
Therefore, an arbitration logic is used. For functional safety, the switch-over
to a fall-back level must be conducted in the presence of any electric and
electronic failure. To provide evidence for a safety argumentation in
compliance with ISO 26262, verification of the arbitration logic is necessary.
The verification process provides confirmation of the correct failure reactions
and that no unintended system states are attainable. Conventional safety
analyses, such as the failure mode and effect analysis, have its limits in this
regard. We present an analytical approach based on formal verification, in
particular model checking, to verify the fail-operational behaviour of a
driving system. For that reason, we model the system behaviour and the relevant
architecture and formally specify the safety requirements. The scope of the
analysis is defined according to the requirements of ISO 26262. We verify a
fail-operational arbitration logic for highly automated driving in compliance
with the industry standard. Our results show that formal methods for safety
evaluation in automotive fail-operational driving systems can be successfully
applied. We were able to detect failures, which would have been overlooked by
other analyses and thus contribute to the development of safety critical
functions.
