劉 峰

（吉林化工學(xué)院，信息與控制工程學(xué)院，吉林 132011）

一個安全并線系統(tǒng)的概率驗證

劉 峰

（吉林化工學(xué)院，信息與控制工程學(xué)院，吉林 132011）

本課題集中研究一個三車并道方案中的簡單協(xié)議。首先通過提出總體的設(shè)想和劃定系統(tǒng)的清晰邊界來定義語言規(guī)則，然后創(chuàng)建參與并道過程的車輛的有限狀態(tài)機，通過基于名為 Zigangorov-Jelinek算法的堆棧算法的概率驗證，我們檢驗?zāi)軌蛱峁┌踩涂煽客ㄐ诺臓顟B(tài)中出現(xiàn)錯誤的可能性。

概率驗證；安全并道；有限狀態(tài)機；Zigangorov-Jelinek算法

0 引言

長久以來，研究者們期望將自動控制巡航系統(tǒng)并入像智能車載高速系統(tǒng)（IVHS）或者智能運輸系統(tǒng)（ITS）這樣的車載系統(tǒng)里。他們致力于模擬真正的高速公路環(huán)境，應(yīng)用先進技術(shù)來控制移動的車輛以減少交通擁堵和事故[1-5]。在研究當中，他們假設(shè)路上所有車輛都配備他們的系統(tǒng)，則總運力的增長超過了1/3。另外，高速公路上常見的行為，像并道這種情況，也在研究當中。一些研究人員開發(fā)出分布式并道算法，使車輛之間能夠在獲得傳感器信息后進行協(xié)商和合作[6-11]。但是，他們的研究都是基于仿真高速公路系統(tǒng)在可靠通訊前提下的通行能力。

我們的研究是在一個可靠的通信協(xié)議之下，定義并道系統(tǒng)內(nèi)的汽車之間的通訊協(xié)議，并用概率驗證來檢驗系統(tǒng)的安全性。本文由六個部分組成：第一部分，我們縱覽和回顧了文獻當中記載的已經(jīng)完成的研究；第二部分，我們用一個以若干假設(shè)為前提的、典型的三車場景描述我們提出的簡單的語言規(guī)則；第三部分，我們展示了為每輛車編制的偽碼；第四部分，通過約簡傳輸層下設(shè)計的協(xié)議，我們給出了簡化的有限狀態(tài)機；第五部分，我們將展示基于堆棧處理過程（即Zigangorov-Jelinek算法）的仿真結(jié)果；最后，我們就未來可能進行的研究提出了一些建議。

1 語言規(guī)則

典型情況下，系統(tǒng)在一個并道過程中包含三輛車：并道車，將被表示為‘M’并位于 1車道。M 想要并入前車（表示為‘F’）和后車（表示為‘B’）所在的2車道。在我們的協(xié)議中，三輛車之間將進行持續(xù)的通信，以便給M提供安全的距離來并入。

在參與并道的三輛車之間有一些假設(shè)：

1. 所有的車都有內(nèi)部計時器。

2. 并道過程開始于M觸發(fā)并道開始按鈕。

3. 所有消息的發(fā)送通過一個可靠的通信層完成。

4. 一旦被鎖定于該并道過程當中，車輛則不能參與一個以上的并道過程。如果車輛已經(jīng)鎖定，任何并道請求將被拒絕。

5. M、F和B都接收和使用相同的傳感器結(jié)果和速度測量值。

6. 在并道過程中，無論是前車還是后車都只能強制減速到安全范圍內(nèi)。

7. 當F和B留出安全距離后，M向駕駛員發(fā)出綠色信號燈。

8. 一些外部變量也需要考慮，例如，如果外部傳感器探測到任何的外來危險或者傳感器被中斷，將會被認為是外部預(yù)警，系統(tǒng)將會中止。

并道過程開始于M的駕駛員按下按鈕而觸發(fā)并道系統(tǒng)。一旦觸發(fā)，M將向F和B發(fā)出鎖定請求。然后，F(xiàn)和B將根據(jù)它們的鎖定情況給予回應(yīng)。只有當F和B都同意鎖定時，M才能繼續(xù)并道過程。一旦三輛車全部鎖定，M將基于傳感器結(jié)果計算所需的安全距離和它們應(yīng)該達到的速度。然后，只有在F和B都達到安全距離并且M接收到對于并道消息的OK確認的條件下，M才能點亮綠色信號燈告知司機終于可以安全的并道了。這時，M的駕駛員才能夠事實上開始并道。

通過規(guī)則的描述，我們發(fā)現(xiàn)F和B是對稱的，它們基本上采取相同的動作。下一部分，我們展示偽碼，這是描述協(xié)議運行最明確的方式。

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)

由于城市總體規(guī)劃水資源論證重點在于論證城市總體規(guī)劃是否符合水資源配置與規(guī)劃，是否存在取水、用水、排水的制約性因素，因此建議地市一級盡快將“三條紅線”指標分解至各區(qū)縣乃至鄉(xiāng)鎮(zhèn)一級，如此方可有效指導(dǎo)和規(guī)范一般范圍較小的城市總體規(guī)劃中的水資源論證工作。

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

下一部分，我們把偽碼翻譯成有限狀態(tài)機。

3 有限狀態(tài)機（FSM）

根據(jù)偽碼，我們生成了M、F和B的有限狀態(tài)機。當輸入變化或超時及外部預(yù)警的情況下，這三個獨立的狀態(tài)機將改變狀態(tài)。在一個可靠的通信協(xié)議下，三個狀態(tài)機互相發(fā)送和接收消息。

消息描述如下：‘m1’是M既發(fā)給F又發(fā)給B的鎖定請求消息；‘r1’是從 F和 B發(fā)出的同意鎖定消息；‘m2’是從F和B發(fā)給M的并道OK信號。

4 概率驗證和仿真結(jié)果

我們使用Matlab為我們的系統(tǒng)做概率驗證，為每一個復(fù)合狀態(tài)設(shè)定六個參數(shù)為：

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

前三個參數(shù)相應(yīng)地代表M、F和B的鎖定狀態(tài)，選項為1（鎖定）和0（未鎖定）。后三個參數(shù)是三輛車的當前狀態(tài)。通過有限狀態(tài)機我們知道，對每輛車來說有4種可能的狀態(tài)，因此將至多有4*4*4=64種組合。然而，在我們定義的系統(tǒng)中不是所有這些組合都可達。我們?yōu)槊恳粋€序列定義的停止狀態(tài)是（0,0,0,0,0,0），意為所有三輛車都從系統(tǒng)中解鎖，并且每當我們在一個序列中遇到一個停止狀態(tài)，我們就停止處理。錯誤狀態(tài)定義為（1,0,0,3,0,0），意為并道車輛實際上正在并道而另外兩輛車已經(jīng)釋放了鎖定。錯誤狀態(tài)應(yīng)該避免并能夠被檢測出來，因為它確實造成了公路上的嚴重威脅。通過給每一個轉(zhuǎn)換指定一個高或低的出現(xiàn)概率，我們能夠找出有多少低概率事件將會最終造成危險。我們假設(shè)計時器不同步和消息丟失是低概率事件，而成功傳送消息是高概率事件。我們使用Zigangorov-Jelinek算法將狀態(tài)入棧，并讓每一個狀態(tài)帶著所有它可能產(chǎn)生的事件出棧。另外，在運行時我們的系統(tǒng)當中存在活鎖，因為幾個狀態(tài)在一個活鎖的方式下將會互相生成，所以我們通過限制同樣狀態(tài)的出現(xiàn)次數(shù)來消除活鎖問題。

最后，我們在兩個下層事件中發(fā)現(xiàn)了錯誤狀態(tài)，就是說兩個低概率事件將導(dǎo)致我們系統(tǒng)的失效。事實上，這個錯誤狀態(tài)是由一個計時器不同步和一個消息丟失引起的。一個產(chǎn)生錯誤序列的可能過程如表1所示。

圖1 并道車Fig.1 The merging car

圖2 前/后車Fig.2 The front/back car

表1 產(chǎn)生錯誤序列的可能過程Tab.1 The possible process of generating error sequences

如表中所示就是產(chǎn)生錯誤狀態(tài)的一種可能序列，而最后兩個低概率事件的轉(zhuǎn)換將導(dǎo)致我們的協(xié)議失效。如果我們給每一個這樣的事件指定概率為10-4，那么危險的概率為 10-8，對于一個安全的并道系統(tǒng)來說還不夠。

5 未來的工作

我們就修正協(xié)議的一些可能的途徑提出建議。一種可能的解決方案是使M中的計時器的延續(xù)時間是F和B的5倍，并且使鎖定的維持時間在原始周期的 1/5以內(nèi)，這樣將降低計時器失效事件的概率至(10-4)5，以便錯誤狀態(tài)可以緩慢地生成。我們還考慮這種可能性：排除F和B的狀態(tài)3的計時器，而是假設(shè)司機將會按下按鈕來釋放鎖定，雖然對于作為人類的司機來說不夠好。

我們不但將仔細考慮每一個轉(zhuǎn)換，而且將找出一個協(xié)議效率的度量辦法，以此來改進規(guī)則。

[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]. 電子科技大學(xué)學(xué)報, 2015, 44(5): 725-730.

[3] 倪捷, 劉志強, 涂孝軍, 董菲. 面向駕駛輔助系統(tǒng)的換道安全性預(yù)測模型研究[J]. 交通運輸系統(tǒng)工程與信息, 2016,16(4): 95-100.

[4] 王世明, 徐建閩, 羅強, 李日涵. 面向高速公路的車輛換道安全預(yù)警模型[J]. 華南理工大學(xué)學(xué)報, 2014, 42(12):40-50.

[5] 李娟, 曲大義, 劉聰?shù)? 基于元細胞自動機的車輛換道行為研究[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] 李珣, 曲仕茹, 夏余. 車路協(xié)同環(huán)境下多車道車輛的協(xié)同換道規(guī)則[J]. 中國公路學(xué)報, 2014, 27(8): 97-104.

[9] 李鵬飛, 石建軍, 劉小明. 城市快速路競爭與協(xié)作換道行為特征分析[J]. 公路交通科技, 2016, 33(12): 130-139.

[10] 向勇, 羅禹貢, 曹坤, 李克強. 基于車-車通信的自動換道控制[J]. 公路交通科技, 2016, 33(3): 120-126, 145.

[11] 楊剛, 張東好, 李克強, 羅禹貢. 基于車車通信的車輛并行協(xié)同自動換道控制[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

本文著錄格式：劉峰. 一個安全并線系統(tǒng)的概率驗證[J]. 軟件，2017，38（12）：119-122

吉林省教育廳重點項目(吉教科合字[2014]第343號)

劉峰(1970-)，男，講師，研究方向：計算機技術(shù)及應(yīng)用。