摘要: 1、研究背景（Context）
近年来，自动驾驶技术取得了飞速的发展，并且已被部署在多个应用领域中。作为一种安全攸关系统，安全性成为了开发自动驾驶系统首要考虑的因素，必须确保车辆在驾驶过程中不会发生碰撞事故。在自动驾驶系统中，车辆的行为控制离不开决策系统的支持，决策系统根据观测到的驾驶场景进行判断，以指挥车辆在下一时刻的动作。目前，智能卡车运输作为自动驾驶领域最有前景的商业用途之一，有不少企业研发了基于自动驾驶的队列系统。队列系统是一个由多辆智能重型卡车组成的多智能体系统，所有车辆排成一列行驶在高速公路上，车辆之间通过实时通信共享道路场景信息，并由队列的决策系统指挥车辆的行为，以此实现协同控制。
形式化方法因其采用数学证明手段对系统进行严谨的建模、验证、规约与推理，被业界应用于系统的安全性验证与分析研究中。然而，目前仍然缺乏有效的形式化方法，来实现对队列系统决策控制层的建模与验证。现有的工作大多只针对单辆车自身的决策控制进行建模与验证，或者只针对队列车辆之间的交互行为进行了安全性验证。因此，十分有必要提出一种可信的方法，以此证明队列驾驶场景下的车队决策系统能安全地控制车辆之间的协同驾驶。
2、目的（Objective）
本文聚焦于跨海高速公路上多辆智能重型卡车组成的队列驾驶系统，针对现有工作无法很好证明队列系统基于场景的决策控制的安全性问题，提出了一个基于队列驾驶场景的决策建模与安全性验证框架，从而保证队列在特定场景下协同驾驶的安全性。
3、方法（Method）
本文基于队列驾驶场景的决策建模与安全性验证框架主要分为以下三个步骤：
首先根据队列驾驶场景的特点，对驾驶场景进行抽象建模，以此表征场景中静态与动态的重要交通特征。然后基于该抽象模型，将前人所提出的多车道空间逻辑（Multi Lane Spatial Logic，MLSL）改进为我们的基本空间逻辑，它可以形式化地描述一般驾驶场景下的道路空间约束条件。
其次，我们从车辆的相对方位和多智能体观测视角两个方面扩展了上述定义的基本空间逻辑，从而得到多智能体空间逻辑（Multi-Agent Spatial Logic，MASL）。我们定义了MASL语言的语法、语义和推理规则，使得MASL公式可以形式化地表述队列驾驶场景下多智能体空间约束规约，作为决策系统的守卫条件。
我们提出了一种适用于队列驾驶机动的形式化建模方法，它采用了基于MASL的时间自动机来构建车辆的决策控制器。其中，决策控制模型的守卫条件集使用了MASL公式来表示队列驾驶场景的空间约束条件。
最后，我们以车辆加入队列的过程作为案例研究，在UPPAAL工具上实现了该模型并验证其安全性质，以此说明本文框架的可行性。
4、结果（Result&Findings）
我们以车辆加入队列的过程为案例，根据所提出的框架规范，在模型检查器UPPAAL上对车辆和与之交互的队列系统的决策控制器进行建模和具体实现。然后通过对模型进行仿真与验证，论述了车辆在行驶过程中如何进行基于场景的决策和协同控制，从而确保队列控制操作的安全性。
根据实验的仿真与验证结果可以得到以下结论：(1)模型是无死锁且可以正确运行的；(2)外来车辆不会因入队条件不满足或者与队列车辆发生碰撞等原因，造成它无法加入到队列；(3)外来车辆在正确的决策控制下最终可以成功加入队列；(4)队列车辆间距能始终保持在安全距离内，既不会因为距离过小导致碰撞、刮擦事故，也不会因为间距过大而导致信号中断、队列断裂；(5)外来车辆加入后形成的新队列仍能保持合理且安全的队内间距。
5、结论（Conclusions）
综上所述，实验结果证明了本文所提出的形式化解决方案可以有效地建模并验证车辆决策控制器的安全性，从而得到一个符合安全规范的队列驾驶决策系统。除了本文所示例的加入队列案例之外，该框架同样适用于解决其它的队列驾驶场景下的决策系统验证问题。
在未来的工作中，我们将继续探索MASL语言的其他重要性质，以建立更加完备的推理系统。我们还将综合考虑队列驾驶场景中的更
多因素来扩展MASL，例如：概率估计、通信时延和故障事件等待，使得MASL语言将能够表征更丰富的场景特征。最后，还有必要开发一套自动化工具来自动验证决策系统在不同驾驶场景下的安全性。