一個(gè)安全并線系統(tǒng)的概率驗(yàn)證

劉 峰

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

一個(gè)安全并線系統(tǒng)的概率驗(yàn)證

劉 峰

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

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

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

0 引言

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

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

1 語言規(guī)則

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

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

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

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

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

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

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

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

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

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

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

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

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ī)劃水資源論證重點(diǎn)在于論證城市總體規(guī)劃是否符合水資源配置與規(guī)劃，是否存在取水、用水、排水的制約性因素，因此建議地市一級(jí)盡快將“三條紅線”指標(biāo)分解至各區(qū)縣乃至鄉(xiāng)鎮(zhèn)一級(jí)，如此方可有效指導(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)機(jī)。

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

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

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

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

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

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

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

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

圖1 并道車Fig.1 The merging car

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

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

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

5 未來的工作

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

我們不但將仔細(xì)考慮每一個(gè)轉(zhuǎn)換，而且將找出一個(gè)協(xié)議效率的度量辦法，以此來改進(jìn)規(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é)報(bào), 2015, 44(5): 725-730.

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

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

[5] 李娟, 曲大義, 劉聰?shù)? 基于元細(xì)胞自動(dòng)機(jī)的車輛換道行為研究[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é)報(bào), 2014, 27(8): 97-104.

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

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

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

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

吉林省教育廳重點(diǎn)項(xiàng)目(吉教科合字[2014]第343號(hào))

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