Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL
Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL
复制标题
DOI：
10.1007/978-3-319-66845-1_4
复制
发表时间：
2017-09
期刊：
影响因子：
--
通讯作者：
Albert Rizaldi;Jonas Keinholz;M. Huber;Jochen Feldle;Fabian Immler;M. Althoff;Eric Hilgendorf;
中科院分区：
文献类型：
--
作者：
Albert Rizaldi;Jonas Keinholz;M. Huber;Jochen Feldle;Fabian Immler;M. Althoff;Eric Hilgendorf;
最近涉及自动驾驶汽车的事故促使我们考虑如何设计一辆始终遵守交通规则的自动驾驶汽车。这尤其具有挑战性，因为交通规则很少按照工程师所期望的详细程度加以规定。因此，要正式监控自动驾驶车辆的行为几乎是不可能的，这些行为是用位置、速度和加速度来表达的，而交通规则则是用模糊的概念来表达的，比如“保持安全距离”。我们将展示如何使用Isabelle定理证明器来实现这一点，首先抽象地编纂交通规则，然后以验证的方式具体化每个原子命题。由于Isabelle的代码生成，我们可以生成用于正式监控交通规则遵守情况的代码。
Recent accidents involving autonomous vehicles prompt us to consider how we can engineer an autonomous vehicle which always obeys traffic rules. This is particularly challenging because traffic rules are rarely specified at the level of detail an engineer would expect. Hence, it is nearly impossible to formally monitor behaviours of autonomous vehicles—which are expressed in terms of position, velocity, and acceleration—with respect to the traffic rules—which are expressed by vague concepts such as “maintaining safe distance”. We show how we can use the Isabelle theorem prover to do this by first codifying the traffic rules abstractly and then subsequently concretising each atomic proposition in a verified manner. Thanks to Isabelle’s code generation, we can generate code which we can use to monitor the compliance of traffic rules formally.