金 麗，章國安，朱 浩，段 瑋，朱曉軍

（南通大學(xué) 信息科學(xué)技術(shù)學(xué)院，江蘇 南通 226019）

道路交通安全問題是車聯(lián)網(wǎng)研究的重要內(nèi)容，專用短程通信IEEE 802.11P 協(xié)議是智能交通系統(tǒng)的重要組成部分[1-5]，它能保證車聯(lián)網(wǎng)中車與車之間短距離通信，大量減少道路上的碰撞事故。IEEE 802.11P 是基于國際標(biāo)準(zhǔn)IEEE 802.11 設(shè)計(jì)的，設(shè)計(jì)中明確以最嚴(yán)格的性能指標(biāo)滿足V2X[6-8]應(yīng)用的所有需求。1999 年，美國聯(lián)邦通信委員會(huì)為V2X在5.9 GHz 區(qū)域中留出75 MHz 的帶寬，并把此作為IEEE 802.11P 標(biāo)準(zhǔn)的工作頻段，該標(biāo)準(zhǔn)于2009 年獲得批準(zhǔn)。IEEE 802.11p 技術(shù)中采用了載波偵聽多路訪問/避免碰撞（carrier sense multiple access with collision avoidance，CSMA/CA）機(jī)制[9-10]，該機(jī)制采用隨機(jī)指數(shù)退避規(guī)則最小化數(shù)據(jù)包傳輸碰撞值。

有關(guān)IEEE 802.11P 通信協(xié)議研究中，Rezgui等[11]人基于分布式協(xié)調(diào)功能（distibuted coordination function，DCF）機(jī)制提出了車輛單位時(shí)間內(nèi)成功接收信息的吞吐量、車輛成功接收信息的概率，以及平均延遲時(shí)間的數(shù)學(xué)推導(dǎo)結(jié)果和模擬數(shù)值仿真分析。Almohammedi 等[12]人通過數(shù)學(xué)推導(dǎo)數(shù)據(jù)包成功發(fā)送的延遲時(shí)間、計(jì)算服務(wù)程序中的飽和吞吐量、數(shù)據(jù)包成功發(fā)送的平均數(shù)量等公式進(jìn)行數(shù)值模擬仿真分析研究IEEE802.11p/1609.4 在車聯(lián)網(wǎng)中的性能。Yao 等[13]人基于IEEE802.11p/1609.4 標(biāo)準(zhǔn)建立了計(jì)算帶寬資源分配的數(shù)學(xué)分析模型，并對(duì)模型進(jìn)行了數(shù)值近似模擬仿真。Gopinath 等[14]人在研究IEEE802.11P/1609.4 標(biāo)準(zhǔn)協(xié)議中提出采用NS3 和SUMO 兩個(gè)仿真工具模擬仿真車輛數(shù)據(jù)傳輸情況。文獻(xiàn)[15-20]通過數(shù)學(xué)推導(dǎo)對(duì)該協(xié)議機(jī)制性能進(jìn)行模擬仿真或數(shù)值分析。本文將使用概率模型檢測(cè)[21-22]來自動(dòng)驗(yàn)證IEEE 802.11P 介質(zhì)訪問控制子協(xié)議，并對(duì)該協(xié)議機(jī)制建立一個(gè)隨機(jī)過程，如馬爾可夫決策過程（Markov decision process，MDP）[23]，概率模型檢測(cè)算法檢測(cè)模型中每個(gè)狀態(tài)是否滿足具體的概率屬性。在模型建立中，選擇使用IEEE 802.11P 介質(zhì)訪問控制方案的雙向握手機(jī)制，它是由兩個(gè)發(fā)送站和兩個(gè)目的站組成的網(wǎng)絡(luò)結(jié)構(gòu)。建模形式為概率時(shí)間自動(dòng)機(jī)（probabilistic timed automata，PTA)[24]，概率時(shí)間自動(dòng)機(jī)是時(shí)間自動(dòng)機(jī)（timed automata，TA）的擴(kuò)展[25]，它的離散概率分布在控制圖的邊緣。為了減少概率模型檢測(cè)中的復(fù)雜度，本文首先采用TA 驗(yàn)證了PTA 中的幾個(gè)抽象模型，由此產(chǎn)生了較小的PTA，采用離散時(shí)間語義屬性得出有限狀態(tài)的馬爾可夫決策過程；然后使用概率模型檢測(cè)工具（probabilistic symbolic model checker，PRISM）[26]來驗(yàn)證重復(fù)傳輸碰撞的可能性和車輛發(fā)送點(diǎn)在一定時(shí)間單元內(nèi)正確發(fā)送數(shù)據(jù)包的概率；最后通過定義相關(guān)到達(dá)概率屬性，進(jìn)行概率模型檢測(cè)。數(shù)值分析結(jié)果表明：車載自組織網(wǎng)絡(luò)基于IEEE 802.11P 通信協(xié)議在短距離數(shù)據(jù)通信傳輸中具有較高的傳輸成功率，在車輛與車輛之間通信中具有良好的鏈路連通性，保證了車載自組織網(wǎng)絡(luò)在一定時(shí)間和距離內(nèi)具有可生存性；另外，所采用的概率模型檢測(cè)器方法與手工運(yùn)算推導(dǎo)公式再進(jìn)行模擬仿真的方法相比，它不僅運(yùn)算效率高、節(jié)省時(shí)間，還可以針對(duì)各個(gè)并行異步模塊組成的非確定性系統(tǒng)建模，從多個(gè)屬性角度進(jìn)行模型分析和數(shù)值仿真。

1 接入技術(shù)

1.1 分布式協(xié)調(diào)功能接入機(jī)制

分布式協(xié)調(diào)功能（distibuted coordination function，DCF）是IEEE 802.11P 通信協(xié)議的信道接入機(jī)制[27-28]，其基于CSMA/CA 協(xié)議，它的一個(gè)重要特征是具有隨機(jī)的、時(shí)隙的指數(shù)退避特征，它旨在打破重復(fù)先前失敗傳輸站點(diǎn)之間的均衡性。

由于IEEE 802.11P 指定發(fā)送站點(diǎn)在傳輸之前偵聽信道，如果多個(gè)站點(diǎn)同時(shí)處于易損期，則可能發(fā)生沖突。例如，如果發(fā)送站點(diǎn)1 處于易損期，當(dāng)它開始發(fā)送數(shù)據(jù)時(shí)，那么其他發(fā)送站點(diǎn)在某種延遲之后（等于易損時(shí)期的長度）才能檢測(cè)到站點(diǎn)1 的傳輸，然而這階段另一個(gè)發(fā)送站點(diǎn)也可能開始傳輸數(shù)據(jù)，這樣就會(huì)導(dǎo)致碰撞。

DCF 有兩種傳輸機(jī)制，分別為基本接入機(jī)制和RTS/CTS 四次握手接入機(jī)制，它們的區(qū)別在于后者在數(shù)據(jù)傳輸之前有RTS 詢問和CTS 應(yīng)答。本文重點(diǎn)研究基本接入機(jī)制，該機(jī)制基本工作原理是：當(dāng)無線局域網(wǎng)絡(luò)中一個(gè)站點(diǎn)準(zhǔn)備發(fā)送一個(gè)新的數(shù)據(jù)包時(shí)，它首先偵聽信道是否在一個(gè)DCF 幀間間隔（distibuted coordination function interfame space，DIFS）內(nèi)空閑，DIFS 的長度取決于物理層并且至少和易損期的長度相等；如果在此期間該信道是空閑的，那么該站點(diǎn)可以向目的站點(diǎn)傳輸數(shù)據(jù)包；在傳輸終止時(shí)，發(fā)送站點(diǎn)立即偵聽信道，以檢測(cè)是否有另一個(gè)站點(diǎn)當(dāng)前正在傳輸，如果有，那么兩站點(diǎn)數(shù)據(jù)包將發(fā)生碰撞，否則該發(fā)送站點(diǎn)等待目的站點(diǎn)發(fā)送一個(gè)確認(rèn)（Ack）信息。因?yàn)榘l(fā)送站點(diǎn)不能監(jiān)聽自身的傳輸，所以目的站點(diǎn)必須發(fā)送確認(rèn)信息，表示數(shù)據(jù)包傳輸成功。為了減少發(fā)送過程中碰撞導(dǎo)致數(shù)據(jù)包傳輸失敗，DCF 將隨機(jī)退避機(jī)制和CSMA/CA 接入方式相結(jié)合，當(dāng)發(fā)送站發(fā)生以下情況之一時(shí)，發(fā)送站將進(jìn)入退避過程：1）發(fā)送站點(diǎn)在一個(gè)DIFS 期間內(nèi)沒有偵聽到信道空閑；2）在發(fā)送站點(diǎn)完成一個(gè)數(shù)據(jù)包傳送后信道仍處于忙狀態(tài)；3）發(fā)送站點(diǎn)在超時(shí)前未接收到目的站點(diǎn)的成功傳輸確認(rèn)信息；4）發(fā)送站點(diǎn)收到確認(rèn)信息又準(zhǔn)備發(fā)送下一個(gè)數(shù)據(jù)包。

1.2 隨機(jī)退避機(jī)制

隨機(jī)退避機(jī)制是一種能降低數(shù)據(jù)包傳輸過程中發(fā)生碰撞的有效方法，它包含退避過程中隨機(jī)退避值的選擇。在隨機(jī)退避過程中，首先，發(fā)送站點(diǎn)需偵聽信道，如果信道忙，那么等待到它處于空閑時(shí)再發(fā)送，這時(shí)還需繼續(xù)進(jìn)行偵聽直到信道空閑為一個(gè)DIFS。接著，隨機(jī)選擇退避值，它表示為“時(shí)隙”的時(shí)間段的數(shù)目。這些時(shí)間段必須通過才能開始傳輸，其中時(shí)隙的持續(xù)時(shí)間是由A slot time 給出的，并且必須至少與易損期一樣長。如果檢測(cè)到信道空閑為一個(gè)A slot time，則退避值將減1 遞減；如果此時(shí)檢測(cè)到信道有數(shù)據(jù)包傳輸，則退避值遞減暫停，直到信道被檢測(cè)到空閑為一個(gè)DIFS，退避值繼續(xù)從原來暫停值處開始遞減直到為0。最后，重新恢復(fù)開始傳輸狀態(tài)。

如圖1 是一個(gè)退避過程應(yīng)用，假設(shè)車聯(lián)網(wǎng)中有4 輛車，分別為車輛1、車輛2、車輛3 和車輛4。車輛1 準(zhǔn)備向目的車輛3 發(fā)送數(shù)據(jù)包，而車輛2 剛完成向目的車輛4 發(fā)送數(shù)據(jù)包，在車輛2 完成傳輸?shù)玫杰囕v4 的確認(rèn)信息后，等待一個(gè)DIFS 時(shí)間繼而隨機(jī)選擇退避值9，然后車輛2 每經(jīng)過一個(gè)A slot time，它的退避值則減1，然而在車輛2 的退避值未減到0 之前車輛1 偵聽到信道在一個(gè)DIFS 時(shí)間內(nèi)是空閑的，它便開始向車輛3 發(fā)送數(shù)據(jù)包，這時(shí)信道處于忙狀態(tài)，車輛2 的當(dāng)前退避值立即暫停減1并保存，等待車輛1 完成數(shù)據(jù)包傳輸，經(jīng)過一個(gè)短幀間隔（short interfame space，SIFS）時(shí)間，得到目的車輛3 的確認(rèn)信息，再經(jīng)過一個(gè)DIFS 時(shí)間后車輛2的退避值在原來暫停保存值上繼續(xù)進(jìn)行減1 直到0。在車輛2 的退避值進(jìn)行暫停到繼續(xù)減1 這一過程稱為凍結(jié)退避值時(shí)間，這個(gè)時(shí)間段信道屬于占用（忙）狀態(tài)。在整個(gè)退避過程中，802.11P 中規(guī)定SIFS 時(shí)間單位小于DIFS 時(shí)間單位，在退避值結(jié)束前發(fā)送站必須要先檢測(cè)信道在一個(gè)DIFS 時(shí)間單位內(nèi)是否空閑。

圖1 車聯(lián)網(wǎng)中兩車節(jié)點(diǎn)間的退避過程Fig.1 Back off procedure between two vehicles in vehicle networks

在上述退避過程中，隨機(jī)退避值的選擇在整數(shù)范圍[0，CW]（爭用窗口）內(nèi)上均勻分布，窗口值計(jì)算公式為CW=（aCWmin+1）× 2bc-1，其中aCWmin是物理層給出的常數(shù)，bc 為變量，表示退避計(jì)數(shù)器，初值設(shè)為0，說明了那些掛起的數(shù)據(jù)包未成功重傳的數(shù)量。退避計(jì)數(shù)器可以設(shè)置一個(gè)上限，用bcmax表示，通過另一個(gè)物理層常數(shù)計(jì)算得到。

2 模型建立

2.1 通信模型建立

本文重點(diǎn)是研究IEEE 802.11P 的DCF 接入機(jī)制中的基本接入機(jī)制。在車聯(lián)網(wǎng)系統(tǒng)中選用任意4輛臨近車節(jié)點(diǎn)，它們相互之間可能存在信息傳輸，其對(duì)應(yīng)車輛通信模型如圖2 所示，包括3 個(gè)模塊，其中車節(jié)點(diǎn)1 和車節(jié)點(diǎn)2 為發(fā)送模塊，車節(jié)點(diǎn)3 和車節(jié)點(diǎn)4 為目標(biāo)接收模塊，以及雙方進(jìn)行信息傳輸?shù)男诺滥K。圖中車節(jié)點(diǎn)1 和車節(jié)點(diǎn)2 共享同一信道分別與車節(jié)點(diǎn)3 和車節(jié)點(diǎn)4 進(jìn)行數(shù)據(jù)通信。由于信道資源共享，容易引起發(fā)送車輛節(jié)點(diǎn)數(shù)據(jù)包碰撞問題而導(dǎo)致雙方通信失敗。為了研究發(fā)送車節(jié)點(diǎn)數(shù)據(jù)傳輸過程產(chǎn)生碰撞問題，基于PTA 理論設(shè)計(jì)了兩個(gè)發(fā)送車節(jié)點(diǎn)的通信信道模型如圖3 所示，圖中兩個(gè)車節(jié)點(diǎn)進(jìn)行數(shù)據(jù)發(fā)送，其中行為狀態(tài)Si包含3 種情況：當(dāng)Si=0 時(shí)，表示信道中無數(shù)據(jù)傳輸；當(dāng)Si=1 時(shí)，表示信道中有數(shù)據(jù)傳輸；當(dāng)Si=2 時(shí)，表示信道中數(shù)據(jù)傳輸混亂（即有數(shù)據(jù)碰撞發(fā)生）。在信道PTA 模型中，i 取值為1 或2，兩個(gè)變量S1和S2分別表示車節(jié)點(diǎn)1 和車節(jié)點(diǎn)2 發(fā)送數(shù)據(jù)包的狀態(tài)，其中車節(jié)點(diǎn)1 發(fā)送時(shí)，用S1:=min（S2+1，2）表示當(dāng)前的狀態(tài)，用S2:=min（S2+S2，2）表示車節(jié)點(diǎn)2 的狀態(tài)；當(dāng)車節(jié)點(diǎn)2 發(fā)送時(shí)，同樣采用類似形式表達(dá)狀態(tài)。信道作為公共資源，既承擔(dān)發(fā)送車節(jié)點(diǎn)的數(shù)據(jù)包傳送任務(wù)，也承擔(dān)著目標(biāo)車節(jié)點(diǎn)收到數(shù)據(jù)包向發(fā)送節(jié)點(diǎn)返回確認(rèn)信息的傳送任務(wù)。

圖2 車輛通信模型Fig.2 Model of the vehicle communication

圖3 車輛信道PTA 模型Fig.3 PTA model of the vehicle channel

2.2 隨機(jī)退避機(jī)制的馬爾可夫決策過程模型建立

車節(jié)點(diǎn)在信道傳輸數(shù)據(jù)過程中遵循IEEE 802.11P 的退避機(jī)制，由于退避過程具有隨機(jī)不確定概率行為，可通過建立MDP 來解決非確定性概率行為。根據(jù)MDP 的定義，建立了發(fā)送車節(jié)點(diǎn)的退避機(jī)制狀態(tài)轉(zhuǎn)換圖，如圖4 所示，車節(jié)點(diǎn)1 檢測(cè)信道空閑（載波偵聽信道），等待一個(gè)DIFS 后，預(yù)約信道，如果此期間內(nèi)超過信道易損期（可能存在發(fā)送節(jié)點(diǎn)2 正傳輸數(shù)據(jù)包），表明信道預(yù)約成功，車節(jié)點(diǎn)1 開始發(fā)送數(shù)據(jù)包，此時(shí)狀態(tài)設(shè)為S1。當(dāng)數(shù)據(jù)包完成傳輸時(shí)間不低于傳送的最小設(shè)置時(shí)間Tmin和不超過傳送的最大設(shè)置時(shí)間Tmax時(shí)，表明數(shù)據(jù)包發(fā)送完成。這時(shí)還需再次檢測(cè)信道在一個(gè)SIFS 內(nèi)是否空閑，如果空閑，即S1+S2=0，那么目標(biāo)車節(jié)點(diǎn)3 給車節(jié)點(diǎn)1 發(fā)送一個(gè)確認(rèn)（Ack）信號(hào)。車節(jié)點(diǎn)1 如果在一個(gè)確認(rèn)時(shí)間Ack_time 內(nèi)收到Ack，則表明發(fā)送任務(wù)成功；否則表明超時(shí)，繼續(xù)等待信道空閑，等待DIFS，進(jìn)入退避過程，退避計(jì)數(shù)器進(jìn)行減1 計(jì)數(shù)，判斷是否過易損期，再次重復(fù)之前信道預(yù)約傳輸數(shù)據(jù)包過程。例如，當(dāng)一個(gè)車節(jié)點(diǎn)發(fā)送完數(shù)據(jù)包準(zhǔn)備再次發(fā)送時(shí)，它必須先等到信道空閑一個(gè)DIFS，如果信道仍忙，則進(jìn)入退避過程，退避計(jì)數(shù)器進(jìn)行隨機(jī)退避計(jì)數(shù)backoff :=RAND{bc}（其中bc 為退避計(jì)數(shù)器的值，它的值不超過退避最大值（bomax=6），退避值在每個(gè)時(shí)隙時(shí)間長度A slot time 上進(jìn)行減1，直到退避計(jì)數(shù)為0，且易損期過后才可再次進(jìn)行數(shù)據(jù)包發(fā)送任務(wù)，具體參數(shù)設(shè)置和描述如表1 所示。

圖4 發(fā)送車節(jié)點(diǎn)MDP 狀態(tài)轉(zhuǎn)換圖Fig.4 MDP status transition diagram of the sending vehicle

表1 參數(shù)設(shè)置和具體描述Tab.1 Notation of the model parameters

2.3 概率時(shí)間自動(dòng)機(jī)模型建立

根據(jù)PTA 的語法和語義規(guī)則[29]，將對(duì)通信模型建立抽象數(shù)學(xué)模型，假設(shè)車載網(wǎng)絡(luò)用PTAVN表示，兩個(gè)發(fā)送車節(jié)點(diǎn)概率時(shí)間自動(dòng)機(jī)模型分別用PTAVS1、PTAVS2表示，信道模型用PTACh表示，目標(biāo)車節(jié)點(diǎn)概率自動(dòng)機(jī)分別用PTAVD1和PTAVD2表示。由于目標(biāo)車節(jié)點(diǎn)行為是確定的，所以把它們組合到發(fā)送車節(jié)點(diǎn)的概率自動(dòng)機(jī)中，分別用PTAVS1′和PTAVS2′表示，其中PTAVS1′=PTAVS1‖PTAVD1，PTAVS2′=PTAVS2‖PTAVD2。另外，數(shù)據(jù)包發(fā)送和確認(rèn)信息都使用同一個(gè)信道進(jìn)行傳輸，信道的自動(dòng)機(jī)可以細(xì)化為PTACh′表示，那么可以得到系統(tǒng)抽象模型為

在抽象模型中，對(duì)于PTA 之前的概率模型，用FPTA（formerly probabilistic timed automaton）來 表示，假設(shè)PTAVN之前的概率模型用FPTAVN來表示，對(duì)于發(fā)送車節(jié)點(diǎn)的PTA 之前的PTA，分別用FPTAVS1和FPTAVS2表示，PTACh之前信道PTA 用FPTACh表示，PTAVD1和PTAVD2分別用FPTAVD1和FPTAVD2表示；同樣對(duì)于PTAVN′而言，它之前的概率模型用FPTAVN表示，PTAVS1′和PTAVS2′之前的概率模型分別用FPTAVS1′和FPTAVS2′表示，PTACh′之前的概率模型用FPTACh′表示，那么得到之前的抽象模型為

經(jīng)過模型檢測(cè)器和轉(zhuǎn)移系統(tǒng)跡分布驗(yàn)證，可以得到

由式（1）—式（5）得出結(jié)論

在IEEE 802.11P 的DCF 基本接入機(jī)制中，由于沒有緊急行為操作，一切的行為操作都是按照預(yù)先設(shè)定的隨機(jī)退避機(jī)制進(jìn)行，所以之前網(wǎng)絡(luò)的PTA表示為LPTA 或LTA。根據(jù)PTA 理論[30-31]可得根據(jù)得到的結(jié)論，通過概率模型檢測(cè)器對(duì)該抽象系統(tǒng)模型在時(shí)間變化上進(jìn)行概率分析，具體通過定義相關(guān)屬性，討論系統(tǒng)模型在不同時(shí)間內(nèi)最小和最大到達(dá)性分析。

3 系統(tǒng)模型概率檢測(cè)

3.1 模型驗(yàn)證

在模型驗(yàn)證過程中，根據(jù)不同的最大退避值bomax和不同的數(shù)據(jù)包傳輸時(shí)間Tmax條件，對(duì)系統(tǒng)狀態(tài)數(shù)、模型建立情況及到達(dá)計(jì)算進(jìn)行統(tǒng)計(jì)和分析。模型分析基于Intel 內(nèi)核、3.4 GHz 處理器、64 位Windows7 版本的操作系統(tǒng)、在PRISM 4.4 模型檢測(cè)器中進(jìn)行。當(dāng)Tmax=500 μs 時(shí)，模型檢測(cè)情況如表2所示，隨著bomax的增大，模型狀態(tài)數(shù)和多終端二元決策圖中的節(jié)點(diǎn)數(shù)也隨之增多，模型建立時(shí)間也隨之變大，迭代數(shù)和迭代時(shí)間也隨之增大。

表2 Tmax=500 μs 下的模型運(yùn)行情況Tab.2 PRISM model checking results with Tmax=500 μs

為了比較在不同bomax下模型檢測(cè)驗(yàn)證情況，考慮增加數(shù)據(jù)包傳輸時(shí)間Tmax的設(shè)定值，當(dāng)Tmax=1 000 μs 和Tmax=2 000 μs 時(shí)，模型運(yùn)行情況分別如表3 和4 所示。

從表3 和4 中可以得出，隨著設(shè)定數(shù)據(jù)包傳輸時(shí)間的變大，對(duì)于相同的bomax，模型狀態(tài)數(shù)、多終端二元決策圖中的節(jié)點(diǎn)數(shù)、模型建立時(shí)間和迭代數(shù)，它們之間的增量隨著Tmax設(shè)定值的變化而不變，多終端二元決策圖中的終端節(jié)點(diǎn)數(shù)隨著Tmax設(shè)定值的變化也保持不變。另外，表1、2 和3 得出同樣的結(jié)果，即模型狀態(tài)數(shù)隨著bomax的增大而增多。

表3 Tmax=1 000 μs 下的模型運(yùn)行情況Tab.3 PRISM model checking results with Tmax=1 000 μs

表4 Tmax=2 000 μs 下的模型運(yùn)行情況Tab.4 PRISM model checking results with Tmax=2 000 μs

3.2 系統(tǒng)模型狀態(tài)到達(dá)概率分析

3.2.1 概率到達(dá)性分析

概率到達(dá)性分析是PRISM 的核心運(yùn)算部分，將產(chǎn)生節(jié)點(diǎn)數(shù)、終端節(jié)點(diǎn)數(shù)和計(jì)算到達(dá)性的迭代數(shù)和迭代時(shí)間。在定義概率到達(dá)性屬性前，PRISM 模型檢測(cè)器對(duì)發(fā)送車節(jié)點(diǎn)的發(fā)送過程狀態(tài)進(jìn)行了描述，具體如表5 所示，一共有12 個(gè)狀態(tài)，其中狀態(tài)11 將在PCTL 概率度量屬性定義運(yùn)用。

表5 車節(jié)點(diǎn)發(fā)送狀態(tài)情況描述Tab.5 Description of the sending vehicle status

具體概率屬性定義公式和模型檢測(cè)結(jié)果如下：

1）屬性定義1 P≥1[ture∪v1=11&v2=11]。式中“≥”是關(guān)系操作，表示下界，與P 的最小概率相對(duì)應(yīng)。該式指在最小概率為1 的情形下兩個(gè)發(fā)送車節(jié)點(diǎn)都成功發(fā)送數(shù)據(jù)包，模型檢測(cè)時(shí)間如表6 所示，隨著bomax的增大，模型檢測(cè)時(shí)間、迭代數(shù)及迭代時(shí)間都增大。

表6 概率到達(dá)性模型檢測(cè)時(shí)間Tab.6 Model checking time of probabilistic reachability

模型驗(yàn)證結(jié)果如圖5 所示，結(jié)果表明車節(jié)點(diǎn)在初始狀態(tài)下滿足屬性要求。

圖5 概率到達(dá)性模型驗(yàn)證結(jié)果Fig.5 Model result of the probabilistic reachability

2）屬性定義2 Pmax=?[ture∪col=k]。該屬性公式表示發(fā)送車節(jié)點(diǎn)碰撞次數(shù)到達(dá)k 的最大概率。表7 中列舉了到達(dá)碰撞次數(shù)分別為2、3、4、5、6 情況下的概率，表中情況說明隨著到達(dá)碰撞次數(shù)越大，發(fā)生的概率越??；當(dāng)碰撞次數(shù)大于4 時(shí)，隨著退避值的增大，發(fā)生的概率一樣。

表7 發(fā)送車節(jié)點(diǎn)碰撞次數(shù)到達(dá)k 的最大概率Tab.7 Maximum probability of k collisions in the sending vehicle

3.2.2 基于時(shí)間邊界的概率到達(dá)性分析

在上述概率分析基礎(chǔ)上，本節(jié)對(duì)模型進(jìn)行時(shí)間邊界的約束，分析了兩個(gè)發(fā)送車節(jié)點(diǎn)在規(guī)定時(shí)間T內(nèi)成功傳輸數(shù)據(jù)包的最小概率情況（最大概率為1），具體屬性公式定義如下：

1）屬性定義3 Pmin1=?[ture∪v1=11&v2=11&t≤T]。該屬性公式表示在規(guī)定時(shí)間T 內(nèi)，兩個(gè)發(fā)送車節(jié)點(diǎn)都能成功完成數(shù)據(jù)包傳輸?shù)淖钚「怕省?/p>

2）屬性定義4 Pmin2=?[ture∪（v1=11v2=11）&t≤T]。該屬性公式表示在規(guī)定時(shí)間T 內(nèi)，兩個(gè)發(fā)送車節(jié)點(diǎn)中任意一個(gè)車節(jié)點(diǎn)成功完成數(shù)據(jù)包傳輸?shù)淖钚「怕省?/p>

3）屬性定義5 Pmin3=?[ture∪v1=11&t≤T]。該屬性公式表示在規(guī)定時(shí)間T 內(nèi)，發(fā)送車節(jié)點(diǎn)1 成功完成數(shù)據(jù)包傳輸?shù)淖钚「怕省?/p>

根據(jù)以上3 個(gè)屬性公式定義，分析了它們?cè)诓煌琓 時(shí)間內(nèi)的模型檢測(cè)概率情況如圖6、7 所示，在圖6 中，數(shù)據(jù)包發(fā)送成功的概率隨時(shí)間變化不同，其中任意一個(gè)車節(jié)點(diǎn)的數(shù)據(jù)包成功傳送率高于兩者同時(shí)傳送的成功率；在圖7 中，在發(fā)送數(shù)據(jù)包完成時(shí)間少的情況下，隨著時(shí)間的增長，車節(jié)點(diǎn)間的數(shù)據(jù)包成功傳送率越大，則網(wǎng)絡(luò)生存性越高；發(fā)送數(shù)據(jù)包的時(shí)間越長，車節(jié)點(diǎn)間的數(shù)據(jù)包成功傳送率越小，那么網(wǎng)絡(luò)生存性越低。研究結(jié)果表明802.11P協(xié)議中的退避算法符合車聯(lián)網(wǎng)節(jié)點(diǎn)通信環(huán)境需求，在短距離傳輸信息上具有很好的表現(xiàn)性。

圖6 T≤100 內(nèi)3 種屬性的最小概率比較Fig.6 Minimum probability comparison of three attributes within T≤100

圖7 T≤100 內(nèi)在不同的傳輸數(shù)據(jù)包最大時(shí)間下最小概率比較Fig.7 Minimum probability comparison of different transmission packets within T≤100

3.2.3 期望到達(dá)性分析

使用Reward 結(jié)構(gòu)用于期望值分析。到達(dá)性的期望屬性定義如下：

1）屬性定義6 Rmax{"col"}=?[Fv1=11&v2=11]。該屬性公式表示在兩個(gè)發(fā)送車節(jié)點(diǎn)成功發(fā)送數(shù)據(jù)包之前的最大期望碰撞次數(shù)，模型檢測(cè)的結(jié)果如表8 所示。在兩個(gè)發(fā)送車節(jié)點(diǎn)成功發(fā)送數(shù)據(jù)包之前，隨著退避值由0～6 變化，到達(dá)性的迭代數(shù)和迭代時(shí)間都隨之增加，但是最大碰撞期望值近似相等，約為1.2 次，不超過兩次，信道傳輸性能良好。

表8 期望最大碰撞數(shù)的模型檢測(cè)結(jié)果Tab.8 Model checking result of expected maximum collision numbers

2）屬性定義7 R1max{"cos t"}=?[Fv1=11&v2=11]。該屬性公式表示在兩個(gè)發(fā)送車節(jié)點(diǎn)都成功發(fā)送數(shù)據(jù)包之前的最大期望丟包數(shù)。模型檢測(cè)的結(jié)果如圖8 所示，當(dāng)最大退避值為0 時(shí)的期望丟包數(shù)最小；當(dāng)最大退避值為1～6 時(shí)，隨著數(shù)據(jù)包最大傳輸時(shí)間的增大，期望丟包數(shù)比最大退避值為0 時(shí)的丟包數(shù)大幅度增長，但是隨著最大退避值大于1，所有的期望丟包數(shù)都近似相等。

3）屬性定義8 R2max{"cos t"}=?[Fv1=1111]。該屬性公式表示在兩個(gè)發(fā)送車節(jié)點(diǎn)中其中一個(gè)車節(jié)點(diǎn)成功發(fā)送數(shù)據(jù)包之前的最大期望丟包數(shù)。模型檢測(cè)結(jié)果如圖9 所示，圖中最大期望丟包數(shù)量隨時(shí)間變化情況和圖8 情況類似。為了進(jìn)一步比較它們兩者的丟包情況，因?yàn)閮烧咴谧畲笸吮苤荡笥?時(shí)最大期望丟包數(shù)近似相等，所以模型檢測(cè)分析針對(duì)兩種情況下最大退避值分別為0 和1 的情形進(jìn)行了比較。具體比較情況如圖10 所示，圖中當(dāng)最大退避值為0 時(shí)，兩車節(jié)點(diǎn)中任一車節(jié)點(diǎn)成功傳輸數(shù)據(jù)包之前的最大期望丟包數(shù)量低于兩車節(jié)點(diǎn)都成功傳輸數(shù)據(jù)包之前的最大期望丟包數(shù)量；當(dāng)最大退避值大于0 時(shí)，兩者最大期望丟包數(shù)量在最大傳輸時(shí)間為300 μs 以內(nèi)時(shí)近似相等；但是當(dāng)最大傳輸時(shí)間大于300 μs 時(shí)，兩車節(jié)點(diǎn)中任一車節(jié)點(diǎn)成功傳輸數(shù)據(jù)包之前的最大期望丟包數(shù)量略低于兩車節(jié)點(diǎn)都成功傳輸數(shù)據(jù)包之前的最大期望丟包數(shù)量，模型檢測(cè)結(jié)果表明滿足屬性公式定義。

圖8 最大期望丟包數(shù)隨時(shí)間的變化曲線（v1＆ v2）Fig.8 Maximum expected number of lost packets with maximum transmission time（v1＆ v2）

圖9 最大期望丟包數(shù)隨時(shí)間的變化曲線（v1│v2）Fig.9 Maximum expected number of lost packets with maximum transmission time（v1│v2）

圖10 兩種發(fā)送情況下最大期望丟包數(shù)隨時(shí)間的變化比較Fig.10 Comparison of maximum expected lost packets in two sending vehicles with maximum transmission time

4 結(jié)論

本文分析了車聯(lián)網(wǎng)短程通信IEEE 802.11P 協(xié)議，研究了分布式協(xié)調(diào)功能DCF 的基本接入技術(shù)，并詳細(xì)分析了該技術(shù)中的雙向握手機(jī)制，使用數(shù)軸圖的形式對(duì)其中的隨機(jī)退避過程進(jìn)行了具體剖析；提出了基于雙向握手機(jī)制的車輛通信系統(tǒng)網(wǎng)絡(luò)模型，根據(jù)該通信網(wǎng)絡(luò)模型的發(fā)送車輛節(jié)點(diǎn)和目標(biāo)車輛節(jié)點(diǎn)的數(shù)據(jù)包傳輸情況，以及信道的使用情況建立了基于概率時(shí)間自動(dòng)機(jī)PTA 的共享信道模型，建立了基于MDP 的隨機(jī)退避過程，并使用概率時(shí)間自動(dòng)機(jī)相關(guān)理論對(duì)隨機(jī)退避過程建立數(shù)學(xué)模型；提出了使用概率模型檢測(cè)方法對(duì)該數(shù)學(xué)模型進(jìn)行檢測(cè)和驗(yàn)證，通過定義相關(guān)滿足約束條件的屬性公式對(duì)模型中各個(gè)狀態(tài)隨時(shí)間變化的到達(dá)概率情況、期望值情況進(jìn)行數(shù)值分析。分析驗(yàn)證結(jié)果表明，車載網(wǎng)絡(luò)在IEEE 802.11P 通信協(xié)議下其短距離數(shù)據(jù)通信傳輸中具有較高的傳輸成功率，在車輛與車輛之間通信中具有良好的鏈路連通性，保證了車載網(wǎng)絡(luò)在一定時(shí)間和距離內(nèi)具有可生存性。另外所提出的概率模型檢測(cè)器方法不同于傳統(tǒng)的手工推導(dǎo)數(shù)學(xué)分析和仿真方法，它能進(jìn)行自動(dòng)狀態(tài)檢測(cè)，在定義各種屬性條件下，它能自動(dòng)完成所有的狀態(tài)搜索、迭代計(jì)算、到達(dá)性分析、基于時(shí)間邊界的各種度量分析，以及期望值分析，這為分析車聯(lián)網(wǎng)通信鏈路連通性提供了借鑒。