一个安全并线系统的概率验证

刘 峰

（吉林化工学院，信息与控制工程学院，吉林 132011）

一个安全并线系统的概率验证

刘 峰

（吉林化工学院，信息与控制工程学院，吉林 132011）

本课题集中研究一个三车并道方案中的简单协议。首先通过提出总体的设想和划定系统的清晰边界来定义语言规则，然后创建参与并道过程的车辆的有限状态机，通过基于名为 Zigangorov-Jelinek算法的堆栈算法的概率验证，我们检验能够提供安全和可靠通信的状态中出现错误的可能性。

概率验证；安全并道；有限状态机；Zigangorov-Jelinek算法

0 引言

长久以来，研究者们期望将自动控制巡航系统并入像智能车载高速系统（IVHS）或者智能运输系统（ITS）这样的车载系统里。他们致力于模拟真正的高速公路环境，应用先进技术来控制移动的车辆以减少交通拥堵和事故[1-5]。在研究当中，他们假设路上所有车辆都配备他们的系统，则总运力的增长超过了1/3。另外，高速公路上常见的行为，像并道这种情况，也在研究当中。一些研究人员开发出分布式并道算法，使车辆之间能够在获得传感器信息后进行协商和合作[6-11]。但是，他们的研究都是基于仿真高速公路系统在可靠通讯前提下的通行能力。

我们的研究是在一个可靠的通信协议之下，定义并道系统内的汽车之间的通讯协议，并用概率验证来检验系统的安全性。本文由六个部分组成：第一部分，我们纵览和回顾了文献当中记载的已经完成的研究；第二部分，我们用一个以若干假设为前提的、典型的三车场景描述我们提出的简单的语言规则；第三部分，我们展示了为每辆车编制的伪码；第四部分，通过约简传输层下设计的协议，我们给出了简化的有限状态机；第五部分，我们将展示基于堆栈处理过程（即Zigangorov-Jelinek算法）的仿真结果；最后，我们就未来可能进行的研究提出了一些建议。

1 语言规则

典型情况下，系统在一个并道过程中包含三辆车：并道车，将被表示为‘M’并位于 1车道。M 想要并入前车（表示为‘F’）和后车（表示为‘B’）所在的2车道。在我们的协议中，三辆车之间将进行持续的通信，以便给M提供安全的距离来并入。

在参与并道的三辆车之间有一些假设：

1. 所有的车都有内部计时器。

2. 并道过程开始于M触发并道开始按钮。

3. 所有消息的发送通过一个可靠的通信层完成。

4. 一旦被锁定于该并道过程当中，车辆则不能参与一个以上的并道过程。如果车辆已经锁定，任何并道请求将被拒绝。

5. M、F和B都接收和使用相同的传感器结果和速度测量值。

6. 在并道过程中，无论是前车还是后车都只能强制减速到安全范围内。

7. 当F和B留出安全距离后，M向驾驶员发出绿色信号灯。

8. 一些外部变量也需要考虑，例如，如果外部传感器探测到任何的外来危险或者传感器被中断，将会被认为是外部预警，系统将会中止。

并道过程开始于M的驾驶员按下按钮而触发并道系统。一旦触发，M将向F和B发出锁定请求。然后，F和B将根据它们的锁定情况给予回应。只有当F和B都同意锁定时，M才能继续并道过程。一旦三辆车全部锁定，M将基于传感器结果计算所需的安全距离和它们应该达到的速度。然后，只有在F和B都达到安全距离并且M接收到对于并道消息的OK确认的条件下，M才能点亮绿色信号灯告知司机终于可以安全的并道了。这时，M的驾驶员才能够事实上开始并道。

通过规则的描述，我们发现F和B是对称的，它们基本上采取相同的动作。下一部分，我们展示伪码，这是描述协议运行最明确的方式。

2 伪码

/*Merging vehicle*/

begin

if (reset)

timer = 0;

lock = 0;

state = s0;

else begin

case (state)

s0: begin

lock = 0; timer = 0;

begin timer;

trigger (ml = lock_request);

state = s1;

end

s1: begin

begin timer;

while (t ＜ timer)

由于城市总体规划水资源论证重点在于论证城市总体规划是否符合水资源配置与规划，是否存在取水、用水、排水的制约性因素，因此建议地市一级尽快将“三条红线”指标分解至各区县乃至乡镇一级，如此方可有效指导和规范一般范围较小的城市总体规划中的水资源论证工作。

wait (rl = lock_agreement);

if (f_lock == 1 && b_lock == 1)

calculate (safe_space);

if (f_can == 1 && b_can == 1)state = s2;

else state = s0;

else state = s0;

end

begin timer;

while (t ＜ timer)

wait (m2 = safe_space_made);

if (m2 == 1) state = s3;

else state = s0;

s3: begin

begin timer;

send (green_light) to the driver;

if (merge_completion == 1 && t ＜ timer)

reset;

else state = s0;

end

end

/*Front/Back vehicle*/

begin

if (reset)

timer = 0;

lock = 0;

state = s0;

else begin

case (state)

s0: begin

begin timer;

if (lock_request == 1 && t ＜ timer)

if (current_lock == 0 && t ＜ timer)state = s1;

else state = s0;

else lock = 0; timer = 0; state = s0;

end

s1: begin

begin timer;

if (b and f in the same lock && t ＜ timer)

calculate if safe_space can be achieved

if (safe_space is possible && t

＜ timer)

state = s2;

else state = s0;

else state = s0;

end

s2: begin

begin timer;

wait (merge_speed);

if (safe_space is achieved && t ＜ timer)

send (m2);

else state = s0;

end

s3: begin

begin timer;

if (t ＜ timer && merge_completion == 1)

reset;

else state = s0;

end

end

下一部分，我们把伪码翻译成有限状态机。

3 有限状态机（FSM）

根据伪码，我们生成了M、F和B的有限状态机。当输入变化或超时及外部预警的情况下，这三个独立的状态机将改变状态。在一个可靠的通信协议下，三个状态机互相发送和接收消息。

消息描述如下：‘m1’是M既发给F又发给B的锁定请求消息；‘r1’是从 F和 B发出的同意锁定消息；‘m2’是从F和B发给M的并道OK信号。

4 概率验证和仿真结果

我们使用Matlab为我们的系统做概率验证，为每一个复合状态设定六个参数为：

（Lm, Lf, Lb, Sm, Sf, Sb）

前三个参数相应地代表M、F和B的锁定状态，选项为1（锁定）和0（未锁定）。后三个参数是三辆车的当前状态。通过有限状态机我们知道，对每辆车来说有4种可能的状态，因此将至多有4*4*4=64种组合。然而，在我们定义的系统中不是所有这些组合都可达。我们为每一个序列定义的停止状态是（0,0,0,0,0,0），意为所有三辆车都从系统中解锁，并且每当我们在一个序列中遇到一个停止状态，我们就停止处理。错误状态定义为（1,0,0,3,0,0），意为并道车辆实际上正在并道而另外两辆车已经释放了锁定。错误状态应该避免并能够被检测出来，因为它确实造成了公路上的严重威胁。通过给每一个转换指定一个高或低的出现概率，我们能够找出有多少低概率事件将会最终造成危险。我们假设计时器不同步和消息丢失是低概率事件，而成功传送消息是高概率事件。我们使用Zigangorov-Jelinek算法将状态入栈，并让每一个状态带着所有它可能产生的事件出栈。另外，在运行时我们的系统当中存在活锁，因为几个状态在一个活锁的方式下将会互相生成，所以我们通过限制同样状态的出现次数来消除活锁问题。

最后，我们在两个下层事件中发现了错误状态，就是说两个低概率事件将导致我们系统的失效。事实上，这个错误状态是由一个计时器不同步和一个消息丢失引起的。一个产生错误序列的可能过程如表1所示。

图1 并道车Fig.1 The merging car

图2 前/后车Fig.2 The front/back car

表1 产生错误序列的可能过程Tab.1 The possible process of generating error sequences

如表中所示就是产生错误状态的一种可能序列，而最后两个低概率事件的转换将导致我们的协议失效。如果我们给每一个这样的事件指定概率为10-4，那么危险的概率为 10-8，对于一个安全的并道系统来说还不够。

5 未来的工作

我们就修正协议的一些可能的途径提出建议。一种可能的解决方案是使M中的计时器的延续时间是F和B的5倍，并且使锁定的维持时间在原始周期的 1/5以内，这样将降低计时器失效事件的概率至(10-4)5，以便错误状态可以缓慢地生成。我们还考虑这种可能性：排除F和B的状态3的计时器，而是假设司机将会按下按钮来释放锁定，虽然对于作为人类的司机来说不够好。

我们不但将仔细考虑每一个转换，而且将找出一个协议效率的度量办法，以此来改进规则。

[1] CHANG T. H., LAI I. S.. Analysis of characteristics of mixed traffic flow of autopilot vehicles and manual vehicles[J]. Transportation Research, 1997, 5(6): 333-348.

[2] 周世杰, 宋竹, 罗嘉庆. 微观交通仿真的安全换道模型研究[J]. 电子科技大学学报, 2015, 44(5): 725-730.

[3] 倪捷, 刘志强, 涂孝军, 董菲. 面向驾驶辅助系统的换道安全性预测模型研究[J]. 交通运输系统工程与信息, 2016,16(4): 95-100.

[4] 王世明, 徐建闽, 罗强, 李日涵. 面向高速公路的车辆换道安全预警模型[J]. 华南理工大学学报, 2014, 42(12):40-50.

[5] 李娟, 曲大义, 刘聪等. 基于元细胞自动机的车辆换道行为研究[J]. 公路交通科技, 2016, 33(11): 140-145.

[6] NI D., LI J., S. Andrews, WANG H.. Preliminary estimate of highway capacity benefit attainable with IntelliDrive technologies[C]//Annual Conference on Intelligent Transportation Systems, 2010.

[7] 曲大义, 陈文娇, 杨万三等. 车辆换道交互行为分析和建模[J]. 公路交通科技, 2016, 33(6): 88-94.

[8] 李珣, 曲仕茹, 夏余. 车路协同环境下多车道车辆的协同换道规则[J]. 中国公路学报, 2014, 27(8): 97-104.

[9] 李鹏飞, 石建军, 刘小明. 城市快速路竞争与协作换道行为特征分析[J]. 公路交通科技, 2016, 33(12): 130-139.

[10] 向勇, 罗禹贡, 曹坤, 李克强. 基于车-车通信的自动换道控制[J]. 公路交通科技, 2016, 33(3): 120-126, 145.

[11] 杨刚, 张东好, 李克强, 罗禹贡. 基于车车通信的车辆并行协同自动换道控制[J]. 公路交通科技, 2017, 34(1): 120-129, 136.

Probabilistic Verification of a Safe Merge System

LIU Feng
(College of information and control engineering, Jilin Institute of Chemical Technology, Jilin 132011, China)

This study focuses the simple protocol in a three-vehicle-merging scenario. First propose an English rule by providing the general assumption and drawing the clear borderline of the system. Then create the Finite State Machines of the vehicles engaged in the merging process. Using probabilistic verification with Stack algorithm,namely Zigangorov-Jelinek algorithm, we test errors state possibilities which offer safe and reliable communication.

Probabilistic verification; Safe merge; Finite state machine; Zigangorov-jelinek algorithm

TP312

A

10.3969/j.issn.1003-6970.2017.12.023

本文著录格式：刘峰. 一个安全并线系统的概率验证[J]. 软件，2017，38（12）：119-122

吉林省教育厅重点项目(吉教科合字[2014]第343号)

刘峰(1970-)，男，讲师，研究方向：计算机技术及应用。