一個安全并線系統的概率驗證

劉 峰

（吉林化工學院，信息與控制工程學院，吉林 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-)，男，講師，研究方向：計算機技術及應用。