A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
复制标题
DOI：
10.1007/978-3-319-40648-0_14
复制
发表时间：
2016-06
期刊：
影响因子：
--
通讯作者：
Albert Rizaldi;Fabian Immler;M. Althoff
中科院分区：
文献类型：
--
作者：
Albert Rizaldi;Fabian Immler;M. Althoff
引入自动驾驶汽车技术的一个障碍是这些车辆发生事故时的责任问题。为了克服这一问题，自动驾驶汽车制造商应该确保他们的车辆始终遵守交通规则。本文主要研究《维也纳道路交通公约》中的安全距离交通规则。确保自动驾驶车辆遵守这一安全距离规则是有问题的，因为维也纳公约没有明确定义安全距离有多大。我们提供了一个经过正式证明的关于该安全距离必须达到多大的规范定义，并对该交通规则的遵从性进行了正确的检查。规定的定义是这样得到的：(1)识别停车(制动)距离的所有可能的相对位置；(2)选择可以推导出碰撞自由度的位置；以及(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.