text: Vehicle safety depends on (a) the range of identified hazards and (b) the operational situations for which mitigations of these hazards are acceptably decreasing risk. Moreover, with an increasing degree of autonomy, risk ownership is likely to increase for vendors towards regulatory certification. Hence, highly automated vehicles have to be equipped with verified controllers capable of reliably identifying and mitigating hazards in all possible operational situations. To this end, available methods for the design and verification of automated vehicle controllers have to be supported by models for hazard analysis and mitigation.
  @cite_3: One barrier in introducing autonomous vehicle technology is the liability issue when these vehicles are involved in an accident. To overcome this, autonomous vehicle manufacturers should ensure that their vehicles always comply with traffic rules. This paper focusses on the safe distance traffic rule from the Vienna Convention on Road Traffic. Ensuring autonomous vehicles to comply with this safe distance rule is problematic because the Vienna Convention does not clearly define how large a safe distance is. We provide a formally proved prescriptive definition of how large this safe distance must be, and correct checkers for the compliance of this traffic rule. The prescriptive definition is obtained by: 1 identifying all possible relative positions of stopping braking distances; 2 selecting those positions from which a collision freedom can be deduced; and 3 reformulating these relative positions such that lower bounds of the safe distance can be obtained. These lower bounds are then the prescriptive definition of the safe distance, and we combine them into a checker which we prove to be sound and complete. Not only does our work serve as a specification for autonomous vehicle manufacturers, but it could also be used to determine who is liable in court cases and for online verification of autonomous vehicles' trajectory planner.
  @cite_10: Autonomous vehicles have found wide-ranging adoption in aerospace, terrestrial as well as marine use. These systems often operate in uncertain environments and in the presence of noisy sensors, and use machine learning and statistical sensor fusion algorithms to form an internal model of the world that is inherently probabilistic. Autonomous vehicles need to operate using this uncertain world-model, and hence, their correctness cannot be deterministically specified. Even once probabilistic correctness is specified, proving that an autonomous vehicle will operate correctly is a challenging problem. In this paper, we address these challenges by proposing a correct-by-synthesis approach to autonomous vehicle control. We propose a probabilistic extension of temporal logic, named Chance Constrained Temporal Logic C2TL, that can be used to specify correctness requirements in presence of uncertainty. We present a novel automated synthesis technique that compiles C2TL specification into mixed integer constraints, and uses second-order quadratic cone programming to synthesize optimal control of autonomous vehicles subject to the C2TL specification. We demonstrate the effectiveness of the proposed approach on a diverse set of illustrative examples.
  @cite_6: One significant barrier in introducing autonomous driving is the liability issue of a collision; e.g. when two autonomous vehicles collide, it is unclear which vehicle should be held accountable. To solve this issue, we view traffic rules from legal texts as requirements for autonomous vehicles. If we can prove that an autonomous vehicle always satisfies these requirements during its operation, then it cannot be held responsible in a collision. We present our approach by formalising a subset of traffic rules from the Vienna Convention on Road Traffic for highway scenarios in Isabelle HOL.
summary: Jha and Raman @cite_10 discuss the synthesis of vehicle trajectories from probabilistic temporal logic assertions. Synthesized trajectories take into account perception uncertainty through approximation of sensed obstacles by combining Gaussian polytopes. In a similar context, Rizaldi and Althoff @cite_6 formalize safe driving policies to derive safe control strategies implementing worst-case braking scenarios in autonomous driving. They apply a hybrid-trace-based formalization of physics required for model checking of recorded @cite_6 and planned @cite_3 strategies. @cite_10 @cite_6 @cite_3 discuss low-level control for a specific class of driving scenarios, whereas our approach provides for (i) the investigation and combination of many related operational situations, thus, forming a more comprehensive perspective of driving safety, (ii) regarding various kinds of hazards that might play a role in high- and low-level control beyond safe and optimal trajectory planning and collision avoidance.