数字交通规则的语义一致性与正确性验证

工程（英文） ›› 2024, Vol. 33 ›› Issue (2) : 55 -71. DOI: 10.1016/j.eng.2023.04.016

研究论文

数字交通规则的语义一致性与正确性验证

万蕾 ¹ ,
王长君 ² ,
罗达新 ¹ ,
刘航 ¹ ,
马莎 ¹ ,
胡伟超 ²

作者信息 +

Semantic Consistency and Correctness Verification of Digital Traffic Rules

Lei Wan ^a ,
Changjun Wang ^b^,^* ,
Daxin Luo ^a ,
Hang Liu ^a ,
Sha Ma ^a ,
Weichao Hu ^b ,

Author information +

文章历史 +

Received	Accepted	Published
2022-08-27	2023-04-06
Issue Date
2024-06-12

PDF (5607K)

摘要

“人车同规”（自动驾驶汽车与人类驾驶汽车遵从相同的交通规则）被汽车行业和交通管理部门视为准则。通过形式化和数字化方法，基于自然语言描述的交通规则可以被转换为数字规则，并被自动驾驶汽车使用。本文提出了一种有效的转换流程，利用分层次的信息提取，可以从丰富而复杂的自然语言语义中提取出交通规则中的有效信息，甚至是隐藏的假设。然而，如何确保转换成的数字规则的准确性，并且与原始交通规则保持一致，是个重要且未被探索过的问题。我们将等价性验证与模型检测相结合，得出了一种行之有效的形式化验证方法。利用本文所提出的交通规则数字化流程和验证方法，可以得到合理、可靠的数字交通规则。在仿真环境中，我们利用这些数字交通规则对车辆行为进行了交规符合性评估。实验结果表明，通过本文所提流程获得的度量时序逻辑描述的数字交通规则，可以很方便地被用于仿真平台和自动驾驶系统中。

Abstract

The consensus of the automotive industry and traffic management authorities is that autonomous vehicles must follow the same traffic laws as human drivers. Using formal or digital methods, natural language traffic rules can be translated into machine language and used by autonomous vehicles. In this paper, a translation flow is designed. Beyond the translation, a deeper examination is required, because the semantics of natural languages are rich and complex, and frequently contain hidden assumptions. The issue of how to ensure that digital rules are accurate and consistent with the original intent of the traffic rules they represent is both significant and unresolved. In response, we propose a method of formal verification that combines equivalence verification with model checking. Reasonable and reassuring digital traffic rules can be obtained by utilizing the proposed traffic rule digitization flow and verification method. In addition, we offer a number of simulation applications that employ digital traffic rules to assess vehicle violations. The experimental findings indicate that our digital rules utilizing metric temporal logic (MTL) can be easily incorporated into simulation platforms and autonomous driving systems (ADS).

关键词

自动驾驶 / 交通规则 / 数字化 / 形式化 / 验证

Key words

Autonomous driving / Traffic rules / Digitization / Formalization / Verification

引用本文

引用格式 ▾

Lei Wan,Changjun Wang,Daxin Luo,Hang Liu,Sha Ma,Weichao Hu,万蕾,王长君,罗达新,刘航,马莎,胡伟超. 数字交通规则的语义一致性与正确性验证[J]. 工程（英文）, 2024, 33(2): 55-71 DOI:10.1016/j.eng.2023.04.016

登录浏览全文

4963

注册一个新账户忘记密码

1 引言

近年来，人们对自动驾驶汽车越来越感兴趣，特别是在自动驾驶系统（ADS）的交通合规性方面。这种兴趣源于自动驾驶汽车与传统汽车一起在公共道路上运行的事实。交通法规是人类社会中无形的管理者，确保了交通流的安全和效率，是绝对必要的。因此，有关部门有必要强制要求自动驾驶汽车遵守人类驾驶员的交通法规。此外，ADS应受完善的法规管理，以确保公共安全[1‒3]。然而，用自然语言描述的人类驾驶员的交通规则有时是主观和不确定的，这使得自动驾驶汽车很难遵守这些规则，因为机器人总是需要客观和具体的数字规则。

规则数字化是将人类驾驶员用自然语言编写的法规转换为计算机可理解的数字方程的过程。有了数字交通规则，交通管理系统将能够对机动车驾驶行为进行自动合规性审查，大大提高交通管理效率。同时，政府相关部门将能够对自动驾驶汽车进行监管测试和评估，以确定车辆是否符合道路行驶的要求，并且汽车制造商的自动驾驶系统开发部门将能够使用数字交通规则。值得注意的是，确保用机器语言表示的交通规则的一致性和正确性是一个极其重要和困难的话题。在这种情况下，“一致性”是指数字交通规则和自然语言交通规则语义等价，描述的是相同的车辆行为和道路环境，而“正确性”是指数字规则可以被机器准确理解，同时避免由于说话技能、人类经验和隐藏的共识等因素导致的自然语言规则量化的不精确和困难。必须确保数字交通规则的一致性和正确性，然后才能使用这些规则来判定非法驾驶行为并做出ADS决策。然而，自然语言和计算机语言是非常不同的，它们之间的翻译非常困难。自然语言处理（NLP）技术已经发展了几十年[4‒5]。此外，计算语言学还考虑了自然语言的统计建模或基于规则的建模[6]。然而，在处理交通法规等严格的文本时，这些技术仍然低于预期[7]。因此，在交通规则数字化的过程中，利用形式化的验证方法来验证数字规则是一个重要和必要的步骤。

2 相关工作

2.1 数字化和规则的实施

时间逻辑（TL）因其安全性和表达性，是实现对规则的合适数字描述的理想选择。TL由一组逻辑形式的集合组成，它们可以描述具有有限状态的系统的特定行为[8]。传统的TL包括线性TL（LTL）、计算树逻辑（CTL）、CTL*、度量TL（MTL）和定时命题TL（TPTL）。LTL，也被称为命题TL，可以用时间模态算子来编码公式[9]。CTL使用树状结构来表示时间模型；它总是被某些模型检测器所使用[10]。作为CTL和LTL的超集，CTL*是分支时间逻辑的一种高级形式[11]。TPTL是一种命题TL，可以用于自然语言规范和形式化验证[12]。作为TL的扩展，MTL [13‒14]经常用于描述对象的行为和情况[15]。MTL是一种灵活的形式表示，可以用于实时系统的时间约束版本[16]。实时逻辑包含对时间的显式引用。它可以表达基于定量定时需求的行为[13,16‒17]，这在描述特定时期的行为时很有用。

在高阶逻辑（HOL）证明助手Isabelle中，Rizaldi和Althoff [18]从《维也纳道路交通公约》中规定了某些公路交通规则，以便将交通规则形式化。Esterle等[19]使用LTL形式化了机器可解释性的交通规则。基于德国道路交通法规，Maierhofer等[20]正式制定了州际交通法规。所有这些例子都是TL的特殊应用。然而，他们缺乏验证信息，来确保他们的方法有利于自然ADS。

Karimi和Duggirala [21]在加州机动车管理局（DMV）的驾驶手册中形式化了某些交通规则，并使用Carla仿真工具仿真了自动驾驶汽车的行为。虽然这项工作很好地实现了交通法规，但它没有检查规则制定的正确性。Beck等[22]使用答案集编程提出了包括一致性测试、诊断和修复的多个任务的实现。然而，这项研究并没有评估关于车辆行驶的交通规则。Krasowski和Althoff [23]还利用TL和使用真实数据评估数字化规则，将《国际海上避碰规则公约》（COLREGS）中的海上交通规则形式化。虽然这项工作令人钦佩，但它缺乏形式化的验证。Esterle等[24]使用LTL中表示的形式化交通规则来验证自动驾驶汽车在语义状态空间中的高级行为，但跳过了这些规则的形式化验证阶段。Hannah等[25]提出在行业标准领域使用谓词逻辑来实现数字交通规则。为了促进命题和逻辑的系统设计，他们将自然语言中的描述符分类为行为、操作设计域（ODD）和假设。该方法可以精确地将自然语言文本转换为谓词逻辑；但是，如果不对场景进行系统的描述，就很容易忽略交通规则的隐含意义。此外，也没有提到对数字交通规则的验证方法。如前所述，有多种方法和逻辑语言可以用来描述交通规则，每一种都具有不同的表达能力和表达形式。然而，大多数方法都缺乏一个可以基于交通流场景的特征来数字化实现所有交通规则的设计流程。

2.2 形式化规则验证

本文将规则形式化作为一种实现ADS交通规则模型的数学技术。确保这些模型的正确性是绝对必要的。在软件工程和集成电路设计领域中，形式化验证总是用于确保设计符合精确陈述的功能正确性概念[26]。形式化验证有利于证明设计的正确性，如软件或硬件系统、程序或模型。它主要是通过定理证明、模型检测和等价性验证来完成的。定理证明——也被称为自动定理证明——是一种使用计算机程序证明数学定理的方法[27]。在数字交通规则模型的形式化验证中，可以将模型形式化为数学方程，然后利用适当的定义和定理推导出这些方程的正确性。另一种方法是模型检测，这也被称为属性检测[28]。在验证系统或模型之前，必须将其形式化为有限状态机（FSM）。通过定义和编程一些属性，机器可以自动检测FSM并识别任何问题[29‒30]。为了自动验证模型和通过算法解决验证问题，系统模型及其性质都必须用精确的数学语言来表示。第三种方法是等价性验证，主要用于硬件验证领域，特别是在集成电路设计开发中[31]。从字面上看，等价模型与系统模型具有相同的功能。理论上，当这两个模型都很准确时，它们的性能应该是相同的。我们还没有发现任何方法或资源来验证数字交通规则的正确性。因此，验证方法是本文最具创新性的方面。本文介绍了在集成电路设计中所使用的形式化验证技术，并提出了一种适用于数字交通规则的新的语义一致性和正确性验证技术。

2.3 贡献

为了保证数字交通规则的一致性和正确性，填补规则验证方法中的技术空白，我们提出了一种数字交通规则形式化验证方法。在本文中，我们开发了一种闭环方法，包括交通规则数字化、形式化验证和仿真测试。这种方法可以提高数字交通规则的权威性、准确性和可访问性。

首先，我们提出了一种交通规则数字化的方法，利用MTL轻松地将现有的交通规则转换为数字规则。为了允许场景和违反条件被分层描述，我们在不同的层次上制定了多个命题，并定义了一个设计数字规则的综合程序。这种方法适用于多种类型的法规，并减少了由于考虑不足而可能导致的错误。

本文的第二个目标是确定如何确保数字交通规则的一致性和正确性。将等价性验证与模型检测相结合，提出了一种形式化验证方法，以保证数字化MTL交通规则合理可靠。在最后一个应用示例中，我们开发了一个仿真平台来测试和验证所提出的数字交通规则。

我们在自动驾驶行业中首次开发了一种针对数字交通规则的形式化验证方法，并成功地完成了在自动驾驶仿真器中对交通规则的形式化实现、验证和应用。

3 数字化、验证和应用程序的概述

图1是本文提出的交通规则的数字化、验证和实施的流程图。整个过程可以分为以下几个部分：①对交通规则进行数字化和形式化，获得数字规则；②对数字规则进行形式化验证，确保其语义一致性和正确性；③将数字规则应用于仿真、现场测试、车辆ADS等场景。首先，使用MTL将交通规则形式化，得到MTL模型，也称为数字交通规则。数字交通规则是将人类司机的交通规则转换成一种计算机可以理解的格式。它们通常描述被明确允许或禁止的行为，与车辆或行人如何感知或评估当前的环境无关。事实上，车辆的行为往往是不可预测的。例如，当车辆在道路上行驶时，可能不清楚它属于哪条车道。有时这是因为状态描述过于宽泛，有时这是因为必须人为地指定车辆状态。在实践中，我们需要合理的定义，以获得特定的状态。在自动驾驶领域，形式化数字交通规则将被用作行为标准或代码。例如，该MTL模型将用于ADS，并将影响车辆的驾驶决策和行为。因此，有必要保证模型的正确性，这就需要对数字规则进行形式化的验证。因此，对数字规则进行形式化验证至关重要。

在形式化验证中，我们将模型检测与等价性验证相结合，以确保MTL模型的一致性和准确性。状态机为动态驾驶行为建模提供了一种强大的方法。对于每个交通规则，我们都设计了一个FSM来描述其规范，以确保行为被精确地表达和理解。因为环境和交通参与者的状态在交通规则中指定了，所以可以使用状态机精确地表示状态之间的转换。状态机有两种方式：首先，将状态机和MTL模型置于等价性检测器中，验证它们的行为一致性；其次，从状态机中提取MTL模型应该具有的一些属性，然后用于模型检测。等价性检测器和模型检测器相互协作，以确保MTL模型的正确性。如果在形式化验证期间发现数字规则的任何问题，则必须修改MTL模型。这个过程将继续进行，直到数字交通规则被证明是准确的为止。

然后在必须检查交通规则的各种场景中实施数字交通规则，包括但不限于：①自动驾驶仿真，用于确定被测试车辆的驾驶轨迹或规划算法是否会导致非法行为；②自动驾驶车辆测试，在测试现场使用仪器或算法来确定被测车辆是否违反规则；③自动驾驶车辆运行，规划算法可使用数字规则来确定其规划路线的合法性，从而防止非法驾驶。

图2描述了一种应用交通规则数字化的方法。为了确定车辆是否违反了交通法规，不仅需要实现数字交通规则，还需要检测软件来解析MTL模型并执行计算。检测器的输入包括环境数据（如天气、道路结构等）、车辆运动轨迹数据和车辆状态数据（如速度和照明数据）。检测器在MTL中解析数字交通规则，根据输入数据确定测试对象是否违反了数字交通规则，并输出交通规则遵守结果。

检测器的输入信息，包括环境、轨迹和状态，可以来自多种来源，包括感知算法、传感器和仿真平台，具体取决于应用。在仿真测试中，如果唯一关注的是车辆是否违反了交通规则，那么输入数据可以直接从仿真软件中获得，而不是像我们在本文中所做的那样，从被测试车辆的感知结果的输出中获取。当检测器在自动驾驶系统中实施时，大部分输入数据只能从传感器和感知算法中收集。在这种情况下，感知算法的精度可能会降低合规结果的精度。本文主要研究交通规则数字化的方法，即设计数字交通规则的过程，并确保数字交通规则与自然语言表达的法律法规的语义一致性。

值得注意的是，交通行为发生在连续的空间中；因此，交通遵从性的计算也应该是连续的。但在实际应用中，我们采用了一种离散化的方法来方便计算：我们在特定的时间间隔对数据进行采样，并计算每个采样点的MTL数字规则。该方法显著提高了性能，简化了软件开发。然而，过大的采样间隔可能会导致误差。例如，如果相邻两个采样点的速度是正常的，那么两个采样点之间潜在的超速行为将不会被识别出来。取样间隔的值是精度和性能之间的折中。

4 交通规则数字化方法

数字交通规则由各种命题和操作符组成。它可以被看作是一个在特定环境中限制车辆行为的数学公式或模型。计算机可以解析和计算公式，以确定被测试车辆的行为是否符合适用的规定。这些命题是数字规则的基本组成部分。在本文中，我们提出了一种能够准确、完整地描述道路环境和交通参与者行为的命题设计方法。

这里使用公制TL来描述数字交通规则。MTL的优点是，它通过使用受时间限制的时序运算符版本来扩展TL，如“直到”和“下一个”运算符[32]。作为一种著名的实时系统的规范形式[33]，MTL非常适合将描述车辆行为的轨迹点集形式化。表1列出了MTL主要的操作符。

本文中使用的交通规则规范来自《中华人民共和国道路交通安全法》[34]、《中华人民共和国道路交通安全法实施条例》[35]和《机动车驾驶人安全文明驾驶操作规范》[36]。本文提出的数字化和验证方法也可应用于其他国家的交通法规和其他各种类型的法规。

4.1 命题的分级和分类

命题表示一种陈述性的行为。对于每个命题p，其中，p∈P和P是一组命题，代表一个布尔语句。换句话说，“一个命题是真理或虚假的非语言载体，使任何表达它的句子成为真或假”[37]。我们根据描述交通场景的需求来制定各种命题。利用Pegasus [38]的6层情景模型，我们将命题分为以下6类：道路模型、基础设施、临时修改、状态描述、行为描述和环境条件。因此，我们可以创建能够非常详细地描述测试环境和场景的命题。如表2所示，我们还创造性地对命题进行了排序和分类，以使数字方法更加层次化。

层次或分级命题的嵌套和调用是由它们的层次或分级性质所促进的。低级命题用于组成高级命题，而编程语言则实现最低级别命题。表3提供了一个使用两种不同的方法描述相同规则的比较示例。使用层次化命题显然可以使规则更简单、更直接、更容易理解。低级命题可以在多个不同的高级命题中重复使用，从而提高实施效率。

4.2 交通规则的数字化

给定上述定义的命题的集合P，任何交通规则φ都可以用MTL来表述。每个数字交通规则都由命题和操作符组成。交通规则数字化的结果——我们称之为数字交通规则——是一个描述允许或禁止行为的公式（称为MTL模型）。图3描述了将交通规则数字化的逐步过程。这种方法可以简化和加快数字化过程，同时防止遗漏条件而导致数字规则出错。

首先，如图3中的步骤1所示，对用自然语言描述的交通规则进行规范化，以获得一个易于计算机解析的定量描述。其次，与步骤2和步骤3一样，我们的方法在描述交通场景时严格遵循6层场景模型。使用静态和动态命题来描述场景，可以获得每个交通参与者的环境状态和行为状态。再次，如步骤4和步骤5所述，使用命题来描述与交通规则对应的判断条件，从而得到最终的数字交通规则。在步骤5之后，输出的是数字流量规则，它是一个MTL语句，也可以被视为一个公式或程序代码。

图3描述了一种轻松、快速地将交通规则数字化，并确保数字化规则的逻辑清晰和语义完整的方法。表4 [34,36]包含了两个数字化结果的例子。表4的内容对应于图3中各步骤的输出，步骤5的输出为最终的数字流量规则。这两种数字交通规则也将被用于随后的形式化验证和仿真测试。

表4显示了规范化规则，它们是自然语言中规则的定量表示。这允许我们在描述交通法规时使用方便的时间和程序表达式。示例1描述了一个关于保持车辆之间的安全距离的交通规则。由于在编程语言中描述主观事物很困难，我们将它们转化为客观表示，这就需要引入距离度量。在本例中，我们使用时间间隔（THW）来定义安全距离[39‒40]。示例2中的交通规则限制了变道行为。与示例1相似，我们使用时间间隔来评估连续变道行为的合理性。在评估MTL格式的数字交通规则时，必须首先使用场景中每个参与者的轨迹信息来计算命题的结果；只有这样才能得到MTL的结果。

5 交通规则的形式化验证

如前所述，数字交通规则必须正确，并在语义上与人类驾驶员的交通规则相一致。因此，我们提出了图4所示的形式化验证方法。本文改进了传统的交通规则验证的定理证明和模型检测方法。定理的推导和验证更适合于定理的证明。Rizaldi等[41]使用Isabelle/HOL对数字交通规则进行形式化和验证。然而，这种方法需要许多基本概念的定义，而且它只对某些类型的交通法规有用。对复杂交通行为使用定理证明方法将使这个任务的难度成倍增加。此外，传统的模型检测器使用FSM来简单地表示系统[42]。对于数字交通规则来说，这是不可接受的做法，因为MTL公式很直观，而且不过于复杂。应该使用数字交通规则本身而不是FSM来确保其正确性。如图4的右半部分所示，所提出的方法主要由两个分支组成，即等价性验证和模型检测，以从多个角度进行形式化验证。首先，可以使用前一节中描述的数字化方法，以一个公式或一段MTL代码的形式获得数字化规则。使用软件工具和特定于场景的数据，可以计算出这个数字规则的结果。使用状态机描述与交通规则相关的问题和交通参与者的行为相关的场景。通过比较状态机的输出和规则计算结果进行等价性验证，可以确定数字流量规则是否正确，如果不正确，则可以确定错误出现在哪里。当进行等价比较时，形式化验证工具遍历所有可能的状态和状态转换，从而覆盖整个状态空间。尽管等价性验证是计算密集型的，并且经常需要运行数小时才能完成，但为了确保数字交通规则的正确性，这是必要的。由于状态机的适应性和彻底性，通过将数字交通规则与FSM比较，可以轻松地修复数字交通规则中的错误。此外，使用这个状态机，就可以抽象和设计一系列流量规则属性。利用这些特性，模型检测可以用来验证数字交通规则。该状态机具有优秀的抽象和描述功能。它可以准确、完整地描述交通状况和车辆状况。虽然它的准确性不能得到绝对的保证，但使用状态图来确定它是否遵守了原来的交通规则是非常简单的。实现一个复杂的状态机需要数百行代码，这使得维护和调试极其困难；因此，FSM不适合作为数字交通规则，而更适合作为验证工具。MTL和状态机是表达交通规则的两种不同的方法。通过将MTL与状态机进行比较，可以简单可行地发现问题。

下面是表4中的示例2的形式化验证示例。

5.1 状态机设计

本节将使用表4示例2中描述的交通规则作为一个实例。这些命题是模型的输入。在本例中，[T]参数量化了两次变道操作之间的时间间隔。通过修改此参数，交通规则的制定者可以调整其重要程度。在实验中，通常采用时间T = 10 s。如果没有这个标准，交通规则是主观的和不可确定的。

如图5所示，ΔT表示两次车道变更之间的间隔，当ΔT ≥ T时，车辆连续进行两次左车道变更，违反了交通规则。通常情况下，当车辆第二次改变左转车道时，就会发出违规通知。

使用表4中的交通规则描述，我们设计了图6中所示的FSM。

这里，STn（n是一个自然数）被用来表示这个FSM中的各种状态。参数t表示车辆停留在当前车道上的时间长度。手动设置一个阈值（TH），以表示车辆在被认为已经返回车道之前必须在车道上停留的时间。当t超过TH时，这种变道行为被认为与之前的变道行为无关，这表明它不是连续的变道。当变道场景开始时，车辆可能处于三种状态之一：在车道内、在左侧交叉车道内，或在右侧交叉车道内。这三个状态分别对应于ST0、ST1和ST3。为了简化状态机，车辆与车道的关系主要用三个状态表示：处于中间车道（ST0），表示车辆可以向左或向右变道；左车道（ST2），表示车辆在最后T秒左转；右车道（ST4），与ST2的情况相反。根据交通规则，当状态为ST2或ST4，车辆在左右车道的停留时间超过T秒时，允许车辆向左右变道，其状态变为ST0，车道停留在中间车道。因此，违反规则的情况可能以两种方式之一发生：要么车辆停留在ST2并再次向左变道（ST2→ST1），要么它停留在ST4并再次向右变道（ST4→ST3）。

例如，如果一辆车辆仍在ST2中，那么它只是至少向左变换了一次车道。如果它第二次左转，将穿过左车道线，处于向左变道的ST1状态。这是一种交通违规行为，所以当信号从ST2变为ST1时，“break”参数变为真。在完成穿越车道线的动作后，车辆返回到ST2。从理论上讲，当车辆穿过一条车道线时，它可以改变车道向左或向右，所以状态机包括了所有与变道相关的情况。此规则不适用于车辆不改变车道而直接向前行驶的情况；我们认为这是在车道上行驶，这属于ST0/ST2/ST4条件。

5.2 属性定义

在提出的验证过程中，MTL模型必须附有一份代表原始自然语言交通规则需求的属性列表。MTL也被用来表示线性状态序列的这些性质[17,29,42]。在正式定义之后，MTL模型将用于自动验证[29]。本节重点介绍使用图6所示的状态机的线性时间行为和设计特性。

等式（1）是根据表4定义的交通规则。此外，根据状态机对车辆行为的描述定义了三个属性，以确保遵守交通法规。这些属性的实现分别在等式（2）~（4）中描述。

T r a f f i c R u l e ≜ a c t C r o s s L e f t ∨ a c t C r o s s R i g h t

→ (a c t C r o s s L e f t ∧ G - T, 0 (¬ a c t C r o s s L e f t

∨ ¬ X (¬ a c t C r o s s R i g h t ⋃ a c t C r o s s (L e f t)))

∨ (a c t C r o s s R i g h t ∧ G - T, 0 (¬ a c t C r o s s R i g h t

(1)

∨ ¬ X (¬ a c t C r o s s L e f t ⋃ a c t C r o s s (R i g h t)))

5.2.1 属性1：变换车道的权利

由于道路结构和驾驶需求的原因，车辆应该有机会向左或向右变道，除非它是在道路的边缘或受到其他交通法规的限制。图7描述了在日常生活中遇到的一种常见的驾驶需求。

因此，MTL模型应该限制变道间隔，而不是完全禁止连续的变道。根据图6所示的FSM，允许车辆在进入ST2/ST4状态后，可以返回左车道或右车道。唯一的限制是，当车辆进行变道时，必须等到状态从ST2/ST4变为ST0后，才被允许再次进行相同的变道行为。

属性1：如果车道变更之间的时间小于[T]秒，则违反交通规则。

P r o p e r t y 1 ≜ T r a f f i c R u l e = = (t 1 - t 0 > D e l t a T i m e

)(2)

在这里，等式（1）定义了TrafficRule。在等式（2）中，t0和t1为车辆在同一方向上穿过车道的时间，DeltaTime为两种变道行为之间的最小间隔，等于等式（1）中的T。由于左右变道情况的相似性，仅提供了左变道示例。

5.2.2 属性2：连续变道

如图8所示，当车辆在有限的时间内改变同一方向的车道不止一次时，除第一次车道外，每次变道都违反交通规则。例如，如果车辆在T秒内向左变换车道三次，则会两次违反规则。

属性2：违规次数取决于车辆变道次数。

P r o p e r t y 2 ≜ ∀ t 0 ∈ 1 … N O W :

I F ∧ A c t C r o s s L e f t t 0 = T R U E

∧ ∀ t 1 ∈ t 0 + 1 … N O W : A c t C r o s s R i g h t t 1 = F A L S E

∧ ∀ t 2 ∈ t 0 + 1 … N O W : A c t C r o s s L e f t t 2 = ¬ A c t C r o s s L e f t t 2 - 1

(3)

T H E N ∧ T r a f f i c R u l e N O W = F A L S E

∧ ∀ t 3 ∈ t 0 + 2 … N O W : T r a f f i c R u l e t 3 = ¬ T r a f f i c R u l e t 3 - 1

E L S E T R U E

在此属性中，如果车辆将状态从ST2/ST4更改为ST1/ST3，无论其处于多少次ST2/ST4状态，都违反规则。

5.2.3 属性3：反向变道

当车辆先向左变道，然后反向变道时会发生什么？FSM表明，在图9所示的模型中，车辆没有违反该交通规则。

属性3：当两个相同的车道变更之间发生相反的变道行为时，不会发生违规。

P r o p e r t y 3 ≜ I F A c t C r o s s L e f t N O W = T R U E T H E N ∀ t 0 ∈ 1 … t - 1 : I F ∧ A c t C r o s s L e f t t 0 = T R U E ∧ ∃ t 1 ∈ t 0 + 1 … t - 1 : A c t C r o s s R i g h t t 1 = T R U E ∧ ∀ t 2 ∈ t 0 + 1 … t - 1 : A c t C r o s s L e f t t 2 = F A L S E T H E N T r a f f i c R u l e N O W = T R U E E L S E T R U E

(4)

根据交通规则，只有当车辆在同一方向穿过两条车道时，该车辆才会违反该规则。因此，如果车道交叉不是连续的，则该行为是可以接受的。这种情况很容易忽略，所以我们设置这个属性来验证MTL模型。

我们提出了上述三个属性作为模型检测示例。为了验证每个数字交通规则，数字交通规则的制定者可以从不同的角度创建各种属性。因为每个交通规则都对应于一个独特的场景，因此必须设计属性和状态机，以确保数字规则的正确性和语义一致性。

5.3 等价检测

MTL和FSM都用于描述相同的交通规则，但它们却完全不同。他们的研究结果表明，交通法规是否被违反，应该是相同的。因此，可以采用一种等价性验证的方法来确保相互之间的正确性。

定义1：状态机和MTL模型的结果必须相同。

C o n s i s t e n c y ≜ ∀ t ∈ 1 … S I M T I M E : T r a f f i c R u l e t

= = ¬ V i o l a t i o n t

(5)

定义1的实现可参见等式（5）。状态机和MTL模型的一致性定义为：在任何时候，它们的输出都表示相同的状态。在等式（5）中有一个逻辑否定符号，因为当违规发生时，等式（1）中的输出“TrafficRule”是“false”，而FSM的状态“violation”是“true”。

6 形式化验证方法的评估

一些形式化验证工具使用静态分析来证明或反证程序的行为符合形式化规范[43]。Temporal Logic of Actions Plus (TLA⁺) [44‒45]和Z [46]是基于状态的描述，强调系统的特性和值。标记转换系统分析器（LTSA）[47]是一个基于事件的规范，它描述了一系列系统事件。SPIN [48]是一种通用的模型验证系统，它是基于状态的，但可以描述一个类似于命令式编程的系统。PRISM [49]也是基于状态的，但引入了一个概率Markov模型。还有其他形式语言，各有利弊。

6.1 评估技术及仪器

TLA⁺是建模系统的最高级别的形式语言。对于数字交通规则的形式化验证，我们采用了TLA⁺。此外，模型检测器TLC是模型检测的标准工具。由于MTL模型、FSM和性质都是用数学方程描述的，因此用TLC进行形式化验证是简单的。由于TLA⁺方程在停顿情况下保持不变，因此Unill和Next运算符在TLA⁺中不可用。等式（1）是在TLA⁺中实现的使用“Any”和“Exist”运算符。图10是一个验证过程的示意图。仿真时间是指每种情况下的状态数。参数IT用来表示采样间隔，即两个状态之间的时间间隔。根据实际情况，IT可以设置为任何时期，如1 s。间隔时间表示在ST2/ST4状态下的时间长度。此外，它对应于两个连续的变道之间允许的最小延迟时间。在形式化验证期间，TLA⁺自动遍历所有路径和状态组合，以确保验证所有可能的情况。当我们将交通规则应用于状态机进行形式化验证时，我们可以在各种情况下验证交通规则的正确性。案例6是一个S形路径，车辆先向左变道，然后向右变道。图6的状态机表明，该场景不会导致违规；但是，如果已验证的交通规则在等式（1）中表示违规，等式（5）的结果为“false”，表示交通规则与状态机不一致，且设计的数字交通规则存在缺陷。

6.2 模型实现

在等式（1）中显示的交通规则模型（1）在TLC中实现。状态机的主要功能是属性定义和等价检测。

6.3 评估结果

我们将IT设置为1 s，仿真时间设置为25 s，间隔时间设置为10 s。允许的间隔时间是指同方向两次变道之间的时间。TLC是检查模块的实施地方。在这次评估中，总共发现了16 666 625个状态，并且没有产生错误或警告。在这个验证流程中，ST1和ST3大约有2 777 540种不同的可能状态，ST2和ST4大约有5 553 740种不同的可能状态。

在这种情况下，交通规则的MTL模型对应于这些属性，并且MTL模型和FSM的输出是完全相同的。形式化验证结果表明，等价性验证和模型验证已成功完成。等式（1）中的数字交通规则与自然语言的交通规则相一致，能够准确地描述违规行为。

6.4 对违反错误数字交通规则的形式化验证

在初始尝试中正确设计MTL方程是一项挑战。在本节中，我们给出一个不正确的数字交通规则的示例，然后使用上一节提出的形式化验证方法来测试其正确性，以确定这种形式化验证方法是否能够准确地识别交通规则中的数字化问题。

T r a f f i c R u l e ≜ a c t C r o s s L e f t ∨ a c t C r o s s R i g h t

→ a c t C r o s s L e f t ∧ G - T, 0 ¬ a c t C r o s s L e f t

(6)

∨ a c t C r o s s R i g h t ∧ G - T, 0 ¬ a c t C r o s s R i g h t

等式（6）是交通规则的另一个应用程序。当车辆穿过车道线时，车辆必须确保近期没有发生类似的行动。

当执行图11所示的验证流程时，有两个冲突：一个在等式（6）和状态机之间；另一个在等式（6）和前面提到的属性3之间。这是因为等式（6）不满足等式（4）所描述的属性。当车辆向左车道变道后，然后转向右车道，再次转向左车道时不应被认为是连续的车道改变，因为右车道改变发生在两个左转之间。属性3很好地描述了这种可接受的行为，但是等式（6）由于没有考虑到上述情况，在图11的步骤5中报告了违规行为。

如果使用等式（1）作为数字规则，则不会出现此验证警告。表5比较了利用这两种数字规则进行形式化验证的结果。

该实验证明了本文提出的方法是有效的。使用形式化验证可以确保交通法规的一致性和正确性。

7 交通规则数字化仿真实验

一旦数字交通规则可用，就可以在各种计算机系统上实施，如：①自动驾驶仿真系统可以获取仿真软件中的车辆轨迹和环境数据，然后使用数字交通规则来确定车辆行为的合法性；②在车辆的实地测试中，由现场或在车辆上的传感器记录相关数据，并可在远程服务器上进行合法性确定；③利用来自传感器和高精度地图提供的数据，自动驾驶系统可以确定车辆在路上行驶时的驾驶轨迹或计划的轨迹是否包括非法行为，并可以修改驾驶行为，以防止非法行为的发生。

利用上述方法，我们可以评估自动驾驶车辆的行驶轨迹是否违反了特定的交通规则。这使得交通管理部门可以确定车辆是否适合上路行驶；数字规则还可以帮助汽车制造商确定他们的产品是否符合交通法规。在本节中，我们将多个数字规则应用于自动驾驶仿真实验，以确定经过仿真器测试的车辆是否违反了这些规则。

7.1 仿真系统的框架

我们在实验中使用的仿真系统的体系结构如图12所示。在虚拟试驾（VTD）自动驾驶仿真软件的基础上，设计并开发了一个仿真车辆行为的仿真平台。由于测试对象与仿真平台相连，因此在仿真中使用了一个自动驾驶系统来控制自我车辆的行为。

此外，我们还创建了一个场景库，包含各种仿真场景，如高速公路路段、十字路口等。场景格式根据OpenDrive [50]和OpenScenario [51]进行了描述。多个数字交通规则同时存储在规则库中，并提供给仿真平台。

在实验中，设计了一个名为Checker的交通规则数字化的软件。从仿真平台中获取各车辆的运动轨迹和环境数据，分析数字交通规则，并确定自我车辆的行为是否违反了这些规则。Checker解析数字交通规则，并使用它们来确定仿真环境的车辆行为是否非法。利用该仿真系统，我们可以确定自动驾驶车辆中由规划算法控制的车辆在仿真环境中运行时是否违反了特定的交通规则。该仿真系统使用了一个工作站（ThinkStation P720），配有Intel Xeon Gold 6134 CPU@3.2GHz和128 GB内存。

7.2 仿真

这里应用了表4中描述的相同的数字交通规则。仿真实验的结果如下所示。

7.2.1 数字规则1：安全距离要求

仿真的内容及结果如图13 [34]所示。为了避免危险，驾驶员必须在同一车道上保持自我车辆和前方车辆之间的安全距离。在图13底部的截图中，蓝色车辆代表自我车辆，到同一车道前方车辆的距离从仿真开始就不断减小。从7.6 s开始，自我车辆与前方车辆之间的距离小于100 m。

因此，Checker可以使用图13中形式化的数字交通规则来确定车辆是否违反了交通规则。

7.2.2 数字规则2：禁止连续变道

在这种情况下，为了到达最右边的车道，自我车辆必须进行两次变道。实验结果如图14所示。很明显，自我车辆连续两次向右换车道，换车道之间只有0.9 s的间隙。Checker用于确定车辆是否违反了在表格顶部列出的数字规则。当车辆第一次换车道时，Checker没有注意到违规行为；然而，当车辆在14.35 s时第二次换车道时，Checker指出违反了交通规则。仿真结果与我们的交通规则定义吻合良好。

7.2.3 数字规则3：行人优先

在这种情况下，行人在3 s标记处开始过马路。车辆没有躲避，而是继续直线向前行驶。实验结果如图15所示。仿真结果表明，当车辆进入人行横道时，它违反了交通规定。实验结果表明，在这些场景中，Checker和数字交通规则能够正确地识别违规行为，并输出违规行为的时间和内容。

8 讨论

授权机构可以使用数字交通规则来评估被测试车辆行为的合规性。在这种情况下，车辆企业需要向被授权的机构提供车辆的运动轨迹和环境数据，以供离线评估。数字交通规则Checker也可以作为自动驾驶系统中的一个模块，用于实时评估车辆的轨迹或由规划模块生成的路径是否符合交通规则。在这种情况下，车辆的合规性结果可能会受到规划和控制模块中的测量误差和不确定性的影响。在这里，我们将简要地讨论这些情况。

8.1 测量误差的影响

在执行交通法规时，不准确的测量可能会导致出现错误。在计算车辆的状况时，经常需要精确的数据，如位置、航向、侧滑和纵向速度。滤波器可以用来消除某些数据波动，如由测量误差引起的位置或速度跳跃。然而，滤波器对一些持续性的错误是无效的，因为它们的特性是模糊的。例如，要通过计算轮胎边缘是否超过车道线的中心来确定车辆是否在车道线上行驶，就需要车辆和车道线的位置。遗憾的是，定位误差（如0.10 m）经常大于车道线宽度的一半（如0.13 m），这使得误判成为可能。

感知和定位技术的发展将减少评估误差。例如，提高车辆姿态估计[52]和侧滑角估计[53]的精度，可以获得更精确的车辆位置和更复杂的高清地图，特别是在全球定位系统（GPS）覆盖的地区或密集的城市地区。这允许获得车辆和车道线之间更精确的相对位置关系。

8.2 动态误差和稳定时间

当自动驾驶系统控制车辆时，由于各种误差和不确定性，实际运动和所需运动之间会发生偏差。动态误差被用来描述这个控制器偏差的发展[54]。当智能车辆启动或进入自动驾驶模式时，控制器通常需要一段时间才能达到稳定状态。这段时间被称为稳定时间。控制器的稳定时间表明它能将稳态误差保持在指定范围内的速度。

当使用数字交通规则来评估车辆的行为时，车辆的稳定状态通常并不重要，因为我们更关心的是车辆的行为是否违反了规则，而不是它为什么会违反规则。因此，在设计数字交通规则时，不考虑动态误差。我们可以假设动态误差在实验中是稳定的。

然而，当在仿真软件或一个测试领域中测试大量的离散场景时，动态误差可能会出现问题。通常，我们只关心车辆在处于稳定状态时违反交通法规的情况。没有必要在达到此条件之前就开始评估。

为了避免动态误差的影响，我们在仿真开始后的短时间内（通常是3 s）开始了实验的合规性评估。这个时间可以被车辆的控制器用来达到一个稳定的状态。在此期间，将不会检测到任何由错误响应导致的违规行为。

8.3 规划中的不确定性

规划是自动驾驶系统的一个复杂模块，它需要对环境的精确感知，理解交通参与者的意图，以及确保在各种场景下稳定安全驾驶。在实际情况下，需要处理大量与前后模块相关的不确定性；此外，感知的局限性、行为预测的偶然性以及与控制的交互性，使得规划的实施更加困难。

在每个状态中使用已知备选方案的确定性决策问题的解决方案相对简单。然而，在现实世界中，其他车辆的行为可能会受到各种不确定性的影响，因此行为可能会产生各种不同的新状态。由于随机状态引起的分岔，随机搜索树比确定性搜索树更复杂。有界不确定性的性能已成为决策模块必须解决的一个重要问题。

在各种场景下，可以分析这种不确定性对交通规则性能和数字化的影响。数字交通规则有两个主要的应用。第一个应用是让交通管理员测试和监控车辆违规行为。在此场景中，车辆状态数据上传到云端或指定服务器，交通管理员离线计算数字交通规则。由于没有实时性要求，因此降低了性能的重要性。

另一个应用是确定自我车辆是否违反或即将违反交通规则。对于前者，计算可以快速执行，因为车辆的行为是由过去决定的；对于后者，由于决策树可能包含大量的行为序列，因此评估每个序列的违规行为具有挑战性。为了提高性能，我们可以利用先验并减少规则的采样空间。例如，基于当前的环境，我们估计了车辆最有可能违反的交通规则，并且只评估了这些规则。

此外，规划模块还必须考虑到交通参与者之间互动的不可预测性。例如，考虑到行人轨迹的不可预测性，确保路上行人的安全是一个重要问题。《中华人民共和国道路交通安全法》规定，车辆必须在人行横道上停车让行[34]。正如第7.2.3节所述，我们在设计数字交通规则时设置了相应的条款。为了避免危险情况的发生，自动驾驶系统可以将这一数字规则作为高成本纳入规划模块。为了防止自动驾驶系统做出危险决策，如果在行为序列中违反了这一规则，系统将受到严厉处罚。

由于数据测量误差和其他不确定因素，在实施数字交通规则时，评估结果会出现波动。如何避免这种影响，提高交通规则评估的鲁棒性，降低评估结果对输入数据的敏感性，是一个非常重要且值得深入研究的课题。未来，我们将在这一领域开展更多研究。

9 结论

交通规则的数字化是自动驾驶汽车与交通规则兼容的关键领域。使用错误的数字交通规则将会严重影响交通安全。因此，应用数字规则的前提是，数字规则必须与人类驾驶员的自然语言交通规则相一致。因此，如何确保数字交通法规的一致性和正确性是一个至关重要的问题。

为了解决这一问题，我们提出了一种将等价性验证与模型检测相结合的新方法。同时，我们描述了数字交通规则的整个设计和应用过程，包括数字化和形式化验证。然后在仿真环境中实现了所设计的数字规则。评估和实验结果表明，自然语言交通规则可以系统地翻译为计算机可理解的TL。我们还演示了MTL交通规则的语义一致性和正确性。这项工作促进了自动驾驶汽车与交通法规的兼容性。

所提出的数字化、验证和应用实验方法有助于当前自动驾驶技术的研究进步，并加快了自动驾驶汽车的实现。在理论上，该方法也可以应用于其他类型的国际交通和驾驶规则。

参考文献

原文顺序 | 出版日期 | 本文引用

[1]	Claybrook J, Kildare S. Autonomous vehicles: no driver...no regulation? Science 2018;361(6397):36‒7. . 10.1126/science.aau2715

[2]	Cummings ML, Britton D. Regulating safety-critical autonomous systems: past, present, and future perspectives. In: Pak R, de Visser EJ, Rovira E, editors. Living with robots. London: Academic Press; 2019. . 10.1016/b978-0-12-815367-3.00006-2

[3]	Nair GS, Bhat CR. Sharing the road with autonomous vehicles: perceived safety and regulatory preferences. Transp Res Part C 2021;122:102885. . 10.1016/j.trc.2020.102885

[4]	Otter DW, Medina JR, Kalita JK. A survey of the usages of deep learning for natural language processing. IEEE Trans Neural Netw Learn Syst 2021;32(2):604‒24. . 10.1109/tnnls.2020.2979670

[5]	Kumar E. Natural language processing. New Delhi: IK International Pvt Ltd; 2011.

[6]	Grishman R. Computational linguistics: an introduction. Cambridge: Cambridge University Press; 1986.

[7]	Liu X, Wu D. From natural language to programming language. In: Goschnick S, editor. Innovative methods, user-friendly tools, coding, and design approaches in people-oriented programming. Hershey: IGI Global; 2018.

[8]	Manna Z, Pnueli A. The temporal logic of reactive and concurrent systems. Berlin: Springer; 1992. . 10.1007/978-1-4612-0931-7_3

[9]	Pnueli A. The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (sfcs 1977); 1977 Oct 31-Nov 1; Providence, RI, USA. New York City: IEEE; 1977. p. 46‒57. . 10.1109/sfcs.1977.32

[10]	Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of the Workshop on Logic of Programs; 1981 May 4‒6; New York City, NY, USA. Berlin: Springer; 1981. P. 52‒71. . 10.1007/bfb0025774

[11]	Emerson EA, Halpern JY. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J Assoc Comput Mach 1986;33(1):151‒78. . 10.1145/4904.4999

[12]	Alur R, Henzinger TA. A really temporal logic. J Assoc Comput Mach 1994;41(1):181‒203. . 10.1145/174644.174651

[13]	Alur R, Henzinger TA. Real-time logics: complexity and expressiveness. Inf Comput 1993;104(1):35‒77. . 10.1006/inco.1993.1025

[14]	Koymans R. Specifying real-time properties with metric temporal logic. Real Time Syst 1990;2(4):255‒99. . 10.1007/bf01995674

[15]	Alur R, Feder T, Henzinger TA. The benefits of relaxing punctuality. J Assoc Comput Mach 1996;43(1):116‒46. . 10.1145/227595.227602

[16]	Ouaknine J, Worrell J. On the decidability of metric temporal logic. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05); 2005 Jun 26‒29; Washington, DC, USA. New York City: IEEE; 2005. p. 188‒97. . 10.1109/lics.2005.33

[17]	Konur S. A survey on temporal logics for specifying and verifying real-time systems. Front Comput Sci 2013;7(3):370‒403. . 10.1007/s11704-013-2195-2

[18]	Rizaldi A, Althoff M. Formalising traffic rules for accountability of autonomous vehicles. In: Proceedings of the 2015 IEEE 18th International Conference on Intelligent Transportation Systems; 2015 Sep 15‒18; Gran Canaria, Spain. New York City: IEEE; 2015. p. 1658‒65. . 10.1109/itsc.2015.269

[19]	Esterle K, Gressenbuch L, Knoll A. Formalizing traffic rules for machine interpretability. In: Proceedings of the 2020 IEEE 3rd Connected and Automated Vehicles Symposium (CAVS); 2020 Oct 4‒5; Victoria, BC, Canada. New York City: IEEE; 2020. p. 1‒7. . 10.1109/cavs51000.2020.9334599

[20]	Maierhofer S, Rettinger AK, Mayer EC, Althoff M. Formalization of interstate traffic rules in temporal logic. In: Proceedings of the 2020 IEEEIntelligent Vehicles Symposium IV); 2020 Oct 19-Nov 13; Las Vegas, NV, USA. New York City: IEEE; 2020. p. 752‒9. . 10.1109/iv47402.2020.9304549

[21]	Karimi A, Duggirala PS. Formalizing traffic rules for uncontrolled intersections. In: Proceedings of the 2020 ACM/IEEE 11th International Conference on CyberPhysical Systems (ICCPS 2020); 2020 Apr 21‍‒‍25; Sydney, NSW, Australia. New York City: IEEE; 2020. p. 41‒50. . 10.1109/iccps48487.2020.00012

[22]

Beck H, Eiter T, Krennwallner T. Inconsistency management for traffic regulations: formalization and complexity results. In: Proceedings of the 13th European Workshop on Logics in Artificial Intelligence; 2012 Sep 26‒28; Toulouse, France. Berlin: Springer; 2012. p. 80‒93. . 10.1007/978-3-642-33353-8_7

[23]	Krasowski H, Althoff M. Temporal logic formalization of marine traffic rules. In: Proceedings of the 2021 IEEEIntelligent Vehicles Symposium IV); 2021 Jul 11‒17; Nagoya, Japan. New York City: IEEE; 2021. p. 186‒92. . 10.1109/iv48863.2021.9575685

[24]	Esterle K, Aravantinos V, Knoll A. From specifications to behavior: maneuver verification in a semantic state space. In: Proceedings of the 2019 IEEEIntelligent Vehicles Symposium IV); 2019 Jun 9‒12; Paris, France. New York City: IEEE; 2019. p. 2140‒7. . 10.1109/ivs.2019.8814241

[25]	Hannah D, Edwards P, Khastgir S. Extended updated proposal for an approach to defining rules of the road. In: Proceedings of the 27th UNECE Functional Requirements for Automated and Autonomous Vehicles (FRAV) Session; 2022 Apr 19‒20; online. Coventry: The University of Warwick; 2022.

[26]	Bjesse P. What is formal verification? ACM SIGDA Newsletter 2005;35(24):1‒34. . 10.1145/1113792.1113794

[27]	Paulson LC. The foundation of a generic theorem prover. J Autom Reason 1989;5(3):363‒97. . 10.1007/bf00248324

[28]	Clarke EM, Grumberg O, Kroening D, Peled D, Veith H. Model checking. 2nd ed. Cambridge: The MIT Press; 2018.

[29]	Baier C, Katoen JP. Principles of model checking. Cambridge: The MIT Press; 2008.

[30]	Visser W, Havelund K, Brat G, Park SJ, Lerda F. Model checking programs. Autom Softw Eng 2003;10(2):203‒32. . 10.1023/a:1022920129859

[31]	Huang SY, Cheng KTT. Formal equivalence checking and design debugging. Berlin: Springer Science & Business Media; 2012.

[32]	Alur R, Henzinger TA. Logics and models of real time: a survey. In: Proceedings of the Symposium of the REX Project (Research and Education in Concurrent Systems); 1991 Jun 3‒7; Mook, The Netherlands. Berlin: Springer; 1991. p. 74‒106. . 10.1007/bfb0031988

[33]	Ouaknine J, Worrell J. Some recent results in metric temporal logic. In: Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems; 2008 Sep 15‒17; Saint Malo, France. Berlin: Springer; 2008. p. 1‒13. . 10.1007/978-3-540-85778-5_1

[34]	National People’s Congress. [Road traffic safety law of the People’s Republic of China]. Beijing: Standing Committee of the National People’s Congress; 2003. Chinese.

[35]	State Council of the People’s Republic of China. [Regulations on the implementation of the road traffic safety law of the People’s Republic of China]. Beijing: Standing Committee of the National People’s Congress; 2004. Chinese.

[36]	The Ministry of Public Security of the People’s Republic of China. GA/T 1773.1‒2021: Operating specifications for safe and civilized motor vehicle drivers. Beijing: The Ministry of Public Security of the People’s Republic of China; 2021. Chinese.

[37]	Ulmasovna ES. The principal use of propositional and suppositional terms in the sentences. JournalNX 2020;6(11):242‒3.

[38]	Scholtes M, Westhofen L, Turner LR, Lotto K, Schuldes M, Weber H, et al. 6-layer model for a structured description and categorization of urban traffic and environment. IEEE Access 2021;9:59131‒47. . 10.1109/access.2021.3072739

[39]	Van Winsum W, Heino A. Choice of time-headway in car-following and the role of time-to-collision information in braking. Ergonomics 1996;39(4):579‒92. . 10.1080/00140139608964482

[40]	Ayres TJ, Li L, Schleuning D, Young D. Preferred time-headway of highway drivers. In: Proceedings of the ITSC 2001. 2001 IEEE Intelligent Transportation Systems; 2001 Aug 25‒29; Oakland, CA, USA. New York City: IEEE; 2001. p. 826‒9. . 10.1109/itsc.2001.948767

[41]

Rizaldi A, Keinholz J, Huber M, Feldle J, Immler F, Althoff M, et al. Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. In: Proceedings of the International Conference on Integrated Formal Methods; 2017 Sep 20‒22; Turin, Italy. Turin, Italy. Berlin: Springer; 2017. p. 50‒66. . 10.1007/978-3-319-66845-1_4

[42]	Schnoebelen P. The complexity of temporal logic model checking. In: Proceedings of the 4th Advances in Modal Logic Conference (AiML 2002); 2002 Sep 30-Oct 2; Toulouse, France. London: King’s College Publications; 2003.

[43]	Habrias H, Frappier M. Software specification methods—an overview using a case study. Berlin: Springer; 2012.

[44]	Kuppe MA, Lamport L, Ricketts D. The TLA⁺ toolbox. 2019. arXiv:10.4204/eptcs.310.6

[45]	Lamport L. Specifying systems: the TLA⁺ language and tools for hardware and software engineers. Boston: Addison-Wesley Professional; 2002. . 10.1109/mc.2002.1033032

[46]	O’Regan G. Concise guide to formal methods. New York City: Springer; 2017. . 10.1007/978-3-319-64021-1_20

[47]

Foster H, Uchitel S, Magee J, Kramer J. LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: OsterweilLJ, RombachHD, SoffaML, editors. Proceedings of the 28th International Conference on Software Engineering; 2006 May 20‒28; Shanghai, China; 2006. p. 771‒4. . 10.1145/1134285.1134408

[48]	Holzmann GJ. The model checker SPIN. IEEE Trans Softw Eng 1997;23(5):279‒95. . 10.1109/32.588521

[49]	Kwiatkowska M, Norman G, Parker D. PRISM: probabilistic symbolic model checker. In: Proceedings of the International Conference on Modelling Techniques and Tools for Computer Performance Evaluation; 2002 Apr 14‒17. London, UK. Berlin: Springer; 2002. p. 200‒4. . 10.1007/3-540-46029-2_13

[50]	Association for Standardization of Automation and Measuring Systems (ASAM e.V.). ASAM OpenDRIVE^® V1.8.0 [Internet]. Hoehenkirchen: ASAM e.V.; 2021 Aug 3 [cited 2023 May 13]. Available from:

[51]	Association for Standardization of Automation and Measuring Systems (ASAM e.V.). ASAM OpenSCENARIO^® V1.2.0 [Internet]. Hoehenkirchen: ASAM e.V.; 2022 May 13 [cited 2023 May 13]. Available from:

[52]	Wu Z, Yao M, Ma H, Jia W. Improving accuracy of the vehicle attitude estimation for low-cost INS/GPS integration aided by the GPS-measured course angle. IEEE Trans Intell Transp Syst 2013;14(2):553‒64. . 10.1109/tits.2012.2224343

[53]	Xia X, Hashemi E, Xiong L, Khajepour A, Xu N. Autonomous vehicles sideslip angle estimation: single antenna GNSS/IMU fusion with observability analysis. IEEE Internet Things J 2021;8(19):14845‒59. . 10.1109/jiot.2021.3072354

[54]	Lynch KM, Park FC. Modern robotics. Cambridge: Cambridge University Press; 2017.

AI Summary AI Mindmap

PDF (5477KB)

2640

访问

被引

Altmetric

详细

导航

在线期刊

作者中心

关于期刊

摘要