  We assume that autonomous or highly automated driving (AD) will be
accompanied by tough assurance obligations exceeding the requirements of even
recent revisions of ISO 26262 or SOTIF. Hence, automotive control and safety
engineers have to (i) comprehensively analyze the driving process and its
control loop, (ii) identify relevant hazards stemming from this loop, (iii)
establish feasible automated measures for the effective mitigation of these
hazards or the alleviation of their consequences.
  By studying an example, this article investigates some achievements in the
modeling for the steps (i), (ii), and (iii), amenable to formal verification of
desired properties derived from potential assurance obligations such as the
global existence of an effective mitigation strategy. In addition, the proposed
approach is meant for step-wise refinement towards the automated synthesis of
AD safety controllers implementing such properties.
