论文标题
使用正式的建模和定时自动机验证数字公路代码
Towards a Digital Highway Code using Formal Modelling and Verification of Timed Automata
论文作者
论文摘要
设计安全，可靠和值得信赖的自动驾驶汽车（AV）的挑战之一是确保AVS遵守交通规则。为此，AVS需要能够理解和推理流量规则。在以前的工作中，我们介绍了空间流量逻辑USL-TR，以允许对流量规则进行明确的机器可读性，正式化。这只是迈向自动交通代理的第一步，可以遵循交通规则。在本研究的预览中，我们关注的另一个步骤：a）直接从交通规则中检索行为图，b）将行为图转换为使用USL-TR公式在后卫和不变式中使用USL-TR公式的定时自动机。这样，我们就可以正式代表交通规则，并可以朝着建立数字公路法规的建立。我们简要设想了进一步的步骤，其中包括将环境和代理模型添加到定时自动机中，以最终使用正式验证工具选择这些流量规则模型。
One of the challenges in designing safe, reliable and trustworthy Autonomous Vehicles (AVs) is to ensure that the AVs abide by traffic rules. For this, the AVs need to be able to understand and reason about traffic rules. In previous work, we introduce the spatial traffic logic USL-TR to allow for the unambiguous, machine-readable, formalisation of traffic rules. This is only the first step towards autonomous traffic agents that verifiably follow traffic rules. In this research preview, we focus on two further steps: a) retrieving behaviour diagrams directly from traffic rules and b) converting the behaviour diagrams into timed automata that are using formulae of USL-TR in guards and invariants. With this, we have a formal representation for traffic rules and can move towards the establishment of a Digital Highway Code. We briefly envision further steps which include adding environment and agent models to the timed automata to finally implement and verify these traffic rule models using a selection of formal verification tools.
