李 堃,張雪松

(1.中國鐵道科學(xué)研究院通信信號(hào)研究所,北京 100081; 2.中國鐵道科學(xué)研究院電子信息研究所,北京 100081)

0 概述

近年來,隨著編組站內(nèi)調(diào)車作業(yè)業(yè)務(wù)量的不斷增大,為減少由于人為操作失誤而造成的“沖、擠、脫”等事故的發(fā)生,無線調(diào)車機(jī)車信號(hào)和監(jiān)控系統(tǒng)(STP)應(yīng)運(yùn)而生[1]。該系統(tǒng)是一種可有效解決上述問題并保證站內(nèi)調(diào)車作業(yè)安全的控制系統(tǒng)[2]。當(dāng)調(diào)車機(jī)車進(jìn)入調(diào)車作業(yè)區(qū)時(shí),機(jī)車接收到點(diǎn)式應(yīng)答器的地面入網(wǎng)信息,并通過無線信道將該信息發(fā)送給系統(tǒng)的地面設(shè)備注冊(cè)入網(wǎng)。地面設(shè)備收到入網(wǎng)申請(qǐng)后,向該機(jī)車發(fā)送確認(rèn)注冊(cè)信息,并分配給機(jī)車一個(gè)入網(wǎng)注冊(cè)號(hào),建立安全控制信息通道,系統(tǒng)進(jìn)入調(diào)車監(jiān)控狀態(tài)。此后,地面設(shè)備根據(jù)調(diào)車機(jī)車所在的位置及開放的調(diào)車信號(hào),通過無線信道向作業(yè)的調(diào)車機(jī)車發(fā)出控制命令。機(jī)車接收到控制命令后,將車列的確切位置、機(jī)車速度、設(shè)備的工作狀態(tài)等有關(guān)信息送回給地面設(shè)備,實(shí)現(xiàn)系統(tǒng)的閉環(huán)控制[3]。

由此可見,安全可靠的車-地之間通信是保證STP系統(tǒng)高效運(yùn)行的關(guān)鍵所在。為此,本文設(shè)計(jì)一種基于STP車-地?zé)o線通信系統(tǒng)的安全通信協(xié)議,以保證傳輸信息的實(shí)時(shí)性、可靠性和完整性。由于國內(nèi)對(duì)于STP系統(tǒng)安全通信協(xié)議的研發(fā)仍處于起步階段,因此本文同時(shí)借鑒ETCS安全通協(xié)議EuroRadio接口規(guī)范[4]并對(duì)其加以創(chuàng)新,設(shè)計(jì)符合STP系統(tǒng)通信需求的安全通信協(xié)議。

1 STP安全通信協(xié)議設(shè)計(jì)

STP是基于車-地之間無線數(shù)傳信道傳輸交互信息,進(jìn)而形成閉環(huán)控制的安全防護(hù)系統(tǒng)。依據(jù)標(biāo)準(zhǔn)EN50159中給出的不同傳輸系統(tǒng)的分類分析STP車-地之間傳輸系統(tǒng)的特征,該通信系統(tǒng)為第3類開放式傳輸系統(tǒng)。EN50159還給出了不同類型傳輸系統(tǒng)可能存在的通信風(fēng)險(xiǎn),以及針對(duì)不同風(fēng)險(xiǎn)推薦的防御手段[5]。表1為常見的威脅-防御矩陣,其中×表示存在的威脅與相應(yīng)的防御措施之間的對(duì)照關(guān)系。據(jù)此,在STP安全通信協(xié)議設(shè)計(jì)中采用序列號(hào)、超時(shí)檢測(cè)、源目的標(biāo)識(shí)、認(rèn)證過程、安全碼等防護(hù)措施,并借鑒ETCS安全相關(guān)系統(tǒng)結(jié)構(gòu)[6],得出STP車-地?zé)o線通信系統(tǒng)結(jié)構(gòu),如圖1所示。

表1 常見威脅-防御矩陣

圖1 STP車-地?zé)o線通信系統(tǒng)結(jié)構(gòu)

1.1 序列號(hào)

STP安全通信協(xié)議采用雙序號(hào)時(shí)間戳防護(hù)機(jī)制[7],以保證車-地傳輸數(shù)據(jù)的實(shí)時(shí)性、完整性和有效性,即在發(fā)送數(shù)據(jù)時(shí),協(xié)議將為其添加2 Byte的序列號(hào)。如用LS、LR分別代表車載設(shè)備的本方序列號(hào)和對(duì)方序列號(hào)(地面設(shè)備序列號(hào)),且各占1 Byte。當(dāng)車載設(shè)備每發(fā)送一包數(shù)據(jù)時(shí),協(xié)議將會(huì)在車載接收到的上一包數(shù)據(jù)中提取本方序列號(hào)LS,并加1,對(duì)方序列號(hào)LR不變。地面設(shè)備在發(fā)送數(shù)據(jù)時(shí)以同樣的方式處理序列號(hào)。

對(duì)于雙方接收到的數(shù)據(jù)包,以車載設(shè)備為例進(jìn)行序列號(hào)有效性檢測(cè)說明。當(dāng)車載設(shè)備接收到新數(shù)據(jù)包后,提取雙序列號(hào):地面本方序列號(hào)DS和地面的對(duì)方序列號(hào)DR。通過if (DS=LR+1)語句,判斷接收數(shù)據(jù)包的連續(xù)性,即檢測(cè)是否出現(xiàn)了數(shù)據(jù)包刪除、插入、亂序等問題;以if(LS-DR<=4)語句保證接收到的數(shù)據(jù)包是在允許延時(shí)范圍內(nèi)的。在STP車-地通信系統(tǒng)中,地面以500 ms為周期發(fā)送控制數(shù)據(jù)給車載。當(dāng)一個(gè)輪詢2 s內(nèi),即4個(gè)周期內(nèi)接收不到車載設(shè)備的回執(zhí)時(shí),認(rèn)為數(shù)據(jù)通信超時(shí)、無效,應(yīng)當(dāng)丟棄[8]。

1.2 超時(shí)檢測(cè)

在周期性信息傳輸系統(tǒng)中,接收信息時(shí)協(xié)議會(huì)檢測(cè)2個(gè)消息之間的時(shí)間間隔是否超過事先確定的最大時(shí)間間隔。若超過,則信息的時(shí)效性得不到保證,就有可能會(huì)給系統(tǒng)帶來危害。

因此,本文在STP安全通信協(xié)議設(shè)計(jì)過程中采用了2種超時(shí)檢測(cè)機(jī)制。一種是數(shù)據(jù)傳輸過程中的雙序號(hào)時(shí)間戳檢測(cè)機(jī)制,該機(jī)制已在1.1節(jié)中給出,這里不再贅述;另一種則是安全連接建立階段的超時(shí)重發(fā)機(jī)制。當(dāng)調(diào)車機(jī)車進(jìn)入調(diào)車作業(yè)區(qū),經(jīng)過入網(wǎng)應(yīng)答器時(shí),車載設(shè)備應(yīng)用進(jìn)程發(fā)起安全連接,請(qǐng)求地面設(shè)備允許其注冊(cè)入網(wǎng),此時(shí),啟動(dòng)車載設(shè)備安全層的安全連接計(jì)時(shí)器。如果在規(guī)定時(shí)間內(nèi),未收到地面的確認(rèn)安全連接請(qǐng)求信息,即分配車載入網(wǎng)注冊(cè)號(hào)信息時(shí),計(jì)時(shí)器溢出,認(rèn)為安全連接超時(shí)。在STP安全通信協(xié)議中,安全連接計(jì)時(shí)器超時(shí)設(shè)定為6 s。當(dāng)計(jì)時(shí)器溢出時(shí),安全層檢測(cè)出車載與地面設(shè)備之間通信超時(shí),便會(huì)在車載設(shè)備報(bào)警之前(6.5 s)自動(dòng)做出響應(yīng),向應(yīng)用進(jìn)程發(fā)送錯(cuò)誤報(bào)告,保證在STP車-地之間通信故障時(shí)及時(shí)導(dǎo)向安全,并請(qǐng)求重新發(fā)起安全連接,從而提高系統(tǒng)通信可靠性。

1.3 源和目的標(biāo)識(shí)

STP車-地通信系統(tǒng)是一個(gè)多端通信系統(tǒng)。因?yàn)樵诖笮途幗M站內(nèi),通常會(huì)有多臺(tái)地面設(shè)備控制不同站場(chǎng)內(nèi)的多臺(tái)調(diào)車機(jī)車同時(shí)作業(yè),所以在使用所接收到的信息之前,需要用合適的方法來檢測(cè)信息的來源。

對(duì)于車-地多端通信系統(tǒng)而言,協(xié)議為每一個(gè)通信端都定義了一個(gè)區(qū)別于其他設(shè)備的唯一標(biāo)識(shí)符。在傳輸信息時(shí),每一包數(shù)據(jù)都攜帶了一個(gè)唯一的源標(biāo)識(shí)和一個(gè)唯一的目的標(biāo)識(shí)[9]。接收端通過接收到的消息中的源和目的標(biāo)識(shí)判斷該消息是否從既定方發(fā)出,以及是否是發(fā)給本方,以此來檢驗(yàn)消息的合法性。

1.4 認(rèn)證機(jī)制

STP安全通信協(xié)議借鑒EuroRadio的2種安全認(rèn)證機(jī)制,一種是安全連接建立階段的對(duì)等實(shí)體認(rèn)證機(jī)制,另一種是數(shù)據(jù)傳輸階段的消息來源認(rèn)證機(jī)制[10],其安全功能參見文獻(xiàn)[6],限于本文篇幅,此處不再贅述。

1.5 安全碼

在STP車-地開放式傳輸系統(tǒng)中,使用安全碼的目的是為了檢測(cè)出信息中的錯(cuò)誤,以此來保證信息的完整性[11]。在本文協(xié)議中采用了CCITT建議的CRC方式,校驗(yàn)結(jié)果置于CRC和CRC2中,其生成多項(xiàng)式為:G(X)=X16+X12+X5+1。

2 安全通信協(xié)議建模

2.1 安全通信協(xié)議時(shí)序圖

安全通信協(xié)議的核心是對(duì)非安全傳輸系統(tǒng)的消息進(jìn)行安全處理,通過不同功能模塊完成各自的安全通信功能,然而每個(gè)功能模塊的核心又是通過管理相應(yīng)的消息收發(fā)時(shí)序?qū)崿F(xiàn)其功能的[12]。STP安全通信協(xié)議的設(shè)計(jì)借鑒了現(xiàn)有成熟EuroRadio的功能結(jié)構(gòu),并在其基礎(chǔ)上加以創(chuàng)新,得到適用于STP車-地通信,且功能完整的安全通信協(xié)議。圖2為EuroRadio安全通信協(xié)議連接建立階段、數(shù)據(jù)傳輸階段、斷開連接階段3個(gè)安全過程的時(shí)序圖。圖3(a)～圖3(c)對(duì)應(yīng)STP安全通信協(xié)議3個(gè)同樣安全過程的時(shí)序圖,圖3(d)則對(duì)應(yīng)STP安全通信協(xié)議新增連接建立超時(shí),故障導(dǎo)向安全功能過程的時(shí)序圖。

圖2 EuroRadio協(xié)議時(shí)序圖

圖3 STP安全通信協(xié)議時(shí)序圖

圖3(a)所示為安全連接建立階段,協(xié)議在EuroRadio安全功能的基礎(chǔ)上,新增了一個(gè)計(jì)時(shí)器功能,用以檢測(cè)安全連接請(qǐng)求自發(fā)起之時(shí)到計(jì)時(shí)器溢出,協(xié)議是否完成了安全連接。

圖3(b)所示為安全數(shù)據(jù)傳輸過程,協(xié)議新增序列號(hào)SN子層(序列號(hào)功能子層)。當(dāng)數(shù)據(jù)發(fā)送方發(fā)送數(shù)據(jù),經(jīng)過SN層時(shí),SN層會(huì)在本方原有序列號(hào)基礎(chǔ)上自增1,但不改變對(duì)方序列號(hào)。隨后SN層將更新后的雙序列號(hào)添加到發(fā)送數(shù)據(jù)中,作為本方用戶數(shù)據(jù)一并發(fā)送給對(duì)方。當(dāng)接收方接收到數(shù)據(jù)時(shí),SN層首先會(huì)對(duì)接收數(shù)據(jù)所攜帶序列號(hào)的時(shí)序性進(jìn)行檢測(cè),以保證發(fā)送給頂層應(yīng)用進(jìn)程的數(shù)據(jù)具有時(shí)效性和完整性。雙序號(hào)時(shí)間戳安全防護(hù)機(jī)制的具體內(nèi)容可參見1.1節(jié)。由于序列號(hào)安全防護(hù)機(jī)制的過程相對(duì)復(fù)雜,鑒于本文篇幅有限,其具體模型建立與模型功能驗(yàn)證本文不做討論。

圖3(c)為斷開安全連接階段,其為應(yīng)用進(jìn)程主動(dòng)發(fā)起斷開安全連接請(qǐng)求場(chǎng)景。如調(diào)車機(jī)車完成了站內(nèi)調(diào)車作業(yè)后,不再需要接收地面發(fā)來的控制命令時(shí),則向地面主機(jī)發(fā)起退網(wǎng)申請(qǐng)。該申請(qǐng)由機(jī)車主機(jī)應(yīng)用進(jìn)程發(fā)起,經(jīng)過機(jī)車安全層,將斷鏈請(qǐng)求發(fā)送至地面設(shè)備。如圖3(c)所示,通過DISCONNCET類4種安全服務(wù)原語,分別斷開機(jī)車主機(jī)、地面主機(jī)各自安全層與應(yīng)用進(jìn)程間的安全連接,以及車載和地面設(shè)備對(duì)等實(shí)體之間的安全連接,使協(xié)議回到初始狀態(tài),等待下次的安全連接,即機(jī)車入網(wǎng)申請(qǐng)的再次發(fā)起。

圖3(d)為STP安全通信協(xié)議新增故障導(dǎo)向安全功能,即:在安全連接建立階段,當(dāng)安全層計(jì)時(shí)器溢出后,安全層檢測(cè)到對(duì)等實(shí)體間仍沒有成功建立安全連接時(shí),視為故障;在數(shù)據(jù)傳輸階段,接收到的數(shù)據(jù)首先經(jīng)安全層新增SN子層的序列號(hào)檢測(cè),如果檢測(cè)不滿足1.1節(jié)中給出的防護(hù)機(jī)制,視為數(shù)據(jù)超時(shí)失效、故障。對(duì)應(yīng)上述2種情況下的故障,安全層均做出響應(yīng),分別向本方應(yīng)用進(jìn)程和對(duì)方安全層發(fā)送Sa-DISCONNECT.indication和T-DISCONNECT.request 2種安全服務(wù)原語,斷開機(jī)車和地面之間的安全連接,跳轉(zhuǎn)到協(xié)議初始狀態(tài)。隨后,發(fā)起方應(yīng)用進(jìn)程便會(huì)自動(dòng)重發(fā)安全連接。

2.2 安全通信協(xié)議Petri模型

本文采用著色Petri網(wǎng)(Colored Petri Net,CPN),依據(jù)“自頂向下”的建模規(guī)則建立STP安全通信協(xié)議分層模型。采用CPN建模的優(yōu)點(diǎn)在于,它不僅可以利用庫所(place)、變遷(transition)和弧(arc)的連接表示系統(tǒng)的靜態(tài)結(jié)構(gòu),還可以通過變遷的觸發(fā)和庫所內(nèi)令牌(token)的遷移,描述系統(tǒng)的動(dòng)態(tài)行為[13]。同時(shí)CPN作為一種高級(jí)Petri網(wǎng),被認(rèn)為是基于網(wǎng)絡(luò)復(fù)雜系統(tǒng)建模和分析的最佳工具[14]。用它建立的模型不但可執(zhí)行,同時(shí)還有利于形式化驗(yàn)證和動(dòng)態(tài)仿真。

圖4顯示了STP安全通信協(xié)議的模型層次結(jié)構(gòu),其中每一個(gè)節(jié)點(diǎn)代表系統(tǒng)中的一個(gè)模型。結(jié)構(gòu)中共包含了8個(gè)模型。除車載和地面安全層子模型和2個(gè)計(jì)時(shí)器子模型外,其他模型均為安全通信協(xié)議運(yùn)行的外部環(huán)境模型。而建立完備的外部環(huán)境模型的目的在于,保證所設(shè)計(jì)的安全通信協(xié)議在滿足EN50159標(biāo)準(zhǔn)的基礎(chǔ)上,方便驗(yàn)證其安全功能是否符合STP車-地之間通信需求,其動(dòng)態(tài)仿真性能參數(shù)是否滿足相應(yīng)安全等級(jí)。

圖4 STP安全通信協(xié)議Petri模型架構(gòu)

在圖5所示的頂層模型中,替代變遷(substitution-transition)Train和替代變遷Ground分別對(duì)應(yīng)機(jī)車與地面的安全功能層。圖6、圖7則給出了安全通信協(xié)議的安全功能執(zhí)行過程,包含從安全連接成功建立后自動(dòng)進(jìn)入數(shù)據(jù)傳輸階段,和機(jī)車完成站場(chǎng)內(nèi)調(diào)車作業(yè)后主動(dòng)申請(qǐng)退網(wǎng)斷開連接的通信過程,其時(shí)序關(guān)系與圖3(a)～圖3(c)所示的時(shí)序圖保持一致。在車載和地面安全層模型中,庫所SafeStatus和庫所Safestatus中包含的令牌值均為:IDLE|WFTC|WFAR|WFAU3|WFRESP|DATA,依次代表其安全層的不同狀態(tài),即:初始狀態(tài)|等待連接狀態(tài)|等待確認(rèn)狀態(tài)|等待AU3原語狀態(tài)|本方已建立安全連接等待對(duì)方打開數(shù)據(jù)鏈路狀態(tài)|安全數(shù)據(jù)傳輸狀態(tài)。圖6和圖7所示模型中的所有變遷分別對(duì)應(yīng)安全層即將進(jìn)入下一狀態(tài)之前會(huì)被觸發(fā)的不同事件。一旦某一變遷(事件)在某一時(shí)刻被觸發(fā),它將決定該時(shí)刻向本方應(yīng)用進(jìn)程和對(duì)方安全層發(fā)送什么類型的服務(wù)原語,以及將本方安全層置于相應(yīng)什么狀態(tài)。從而保證安全層不同狀態(tài)之間的連續(xù)自動(dòng)轉(zhuǎn)換,和安全功能的連續(xù)有效執(zhí)行。

圖8給出了車載安全層的計(jì)時(shí)器模型。由于車載與地面安全層計(jì)時(shí)器功能一樣,因此本文以車載為例,僅給出車載安全層計(jì)時(shí)器模型。如圖8所示,庫所T的初始令牌值為6,它表示安全連接最大超時(shí)時(shí)間為6 s。庫所FULL代表計(jì)時(shí)器超時(shí)溢出狀態(tài),因此,當(dāng)庫所FULL中包含令牌值時(shí),計(jì)時(shí)器模型此時(shí)便會(huì)檢測(cè)庫所Status中的令牌值是否為DATA。如果是,則表示安全連接已在6 s內(nèi)成功建立,安全層此時(shí)不發(fā)送錯(cuò)誤報(bào)告;如果庫所Status中的令牌值是除DATA外的其他任一值時(shí),均認(rèn)為安全連接超時(shí),那么變遷ReLink此時(shí)將會(huì)被觸發(fā),向本方應(yīng)用進(jìn)程發(fā)送連接錯(cuò)誤報(bào)告,并申請(qǐng)重新發(fā)起安全連接,保證系統(tǒng)故障導(dǎo)向安全,其時(shí)序關(guān)系與圖3(d)連接超時(shí)故障導(dǎo)向安全時(shí)序邏輯保持一致。

圖5 STP安全通信協(xié)議頂層模型

圖6 車載安全層模型

圖7 地面設(shè)備安全層模型

圖8 安全層計(jì)時(shí)器模型

3 基于ASK-CTL的形式化驗(yàn)證

安全通信協(xié)議功能的正確性取決于協(xié)議能否做出正確響應(yīng),且以正確的順序響應(yīng)事件。而協(xié)議的邏輯表示的是狀態(tài)轉(zhuǎn)換的過程,因此,安全通信協(xié)議的功能驗(yàn)證,即驗(yàn)證協(xié)議是否以正確的事件發(fā)生次序到達(dá)期望狀態(tài)。時(shí)序邏輯是與模型檢測(cè)緊密相關(guān)的概念,用來刻畫有限狀態(tài)系統(tǒng)中事件發(fā)生的時(shí)序關(guān)系。

據(jù)此,本節(jié)首先利用CPN.Tools建模工具生成第2節(jié)中給出的Petri模型的狀態(tài)空間可達(dá)圖,同時(shí)將待驗(yàn)證的安全功能性質(zhì)表達(dá)成形式化時(shí)序邏輯描述語言:ASK-CTL公式。最后通過狀態(tài)空間搜索算法檢驗(yàn)?zāi)Ｐ蜖顟B(tài)空間可達(dá)圖上是否存在滿足此性質(zhì)的狀態(tài)節(jié)點(diǎn)。結(jié)果為真,則證明安全通信協(xié)議滿足該性質(zhì);反之,不滿足,找出原因,并對(duì)安全通信協(xié)議做出相應(yīng)改進(jìn)。

3.1 ASK-CTL相關(guān)定義

計(jì)算樹時(shí)序邏輯(Computational Tree Logic,CTL)是一種典型的分支時(shí)序邏輯,是被作為描述有限狀態(tài)系統(tǒng)的一種聲明語言[15]。在描述系統(tǒng)狀態(tài)轉(zhuǎn)換的性質(zhì)方面,CTL具有很強(qiáng)的規(guī)范描述邏輯。它用時(shí)態(tài)算子描述沿計(jì)算路徑的狀態(tài)變化,用路徑算子解釋時(shí)間分支性質(zhì)[16]。而ASK-CTL僅是CTL邏輯的一種擴(kuò)展,因此與CTL具有很多共同的時(shí)序邏輯。

ASK-CTL狀態(tài)公式的語法如下:

A::= tt|α|A|A1∨A2|EU(A1,A2)|AU(A1,A2)=

tt|α|NOT(A)|A1∪A2|EU(A1,A2)|AU(A1,A2)

為構(gòu)造復(fù)雜的系統(tǒng)時(shí)序邏輯表達(dá)式,ASK-CTL還有以下擴(kuò)展操作符:

POS A=EU(tt,A)=EXIST_UNTIL(tt,A):表示存在一條路徑,可以到達(dá)一個(gè)狀態(tài),使得A成立;

INV A=POSA=NOT(POS(NOT A)):表示沒有路徑可以達(dá)到一個(gè)狀態(tài),使得A的反命題成立,即對(duì)于每一個(gè)可達(dá)狀態(tài),A成立;

EV A=AU(tt,A)=FORALL_UNTIL(tt,A):表示對(duì)于所有路徑,在有限步內(nèi)使A成立;

ALONG A=EVA=NOT(EV(NOT A)):表示存在一條路徑在有限步內(nèi)使A的反命題成立,即存在一條無限路徑,路徑中的每個(gè)狀態(tài)都使得A成立。

3.2 形式化驗(yàn)證

通常系統(tǒng)待驗(yàn)證的目標(biāo)屬性可分為兩大類,即可操作性和安全性[17]。所謂可操作性,即系統(tǒng)期待的狀態(tài)最終會(huì)出現(xiàn);而安全性描述的則是危害系統(tǒng)的壞事情永遠(yuǎn)不會(huì)發(fā)生的屬性。

結(jié)合STP安全通信協(xié)議所具備的安全功能屬性,本文將協(xié)議待驗(yàn)證的屬性歸納為:1)安全連接建立過程的可操作性;2)數(shù)據(jù)傳輸過程的可操作性;3)安全連接建立過程的安全性;4)數(shù)據(jù)傳輸過程的安全性;5)故障導(dǎo)向安全屬性。前4個(gè)屬性的驗(yàn)證是基于車載安全層與地面安全層Petri模型實(shí)現(xiàn)的,其模型對(duì)應(yīng)圖6和圖7。此時(shí)的驗(yàn)證不包含對(duì)圖8所示的連接超時(shí)計(jì)時(shí)功能模型的檢驗(yàn)。而最后一個(gè)屬性的驗(yàn)證則是建立在完備安全通信協(xié)議模型的基礎(chǔ)上實(shí)現(xiàn)的,即在圖6～圖8所示原有安全層模型上添加連接超時(shí)檢測(cè)子模型,具體過程如圖9所示。

圖9 安全連接建立過程可操作性驗(yàn)證

如圖9所示,安全連接建立過程的可操作性形式化驗(yàn)證步驟如下:

步驟1函數(shù)LinkTrain和函數(shù)LinkGround分別描述機(jī)車和地面設(shè)備應(yīng)用層被期望到達(dá)的狀態(tài)[CONED],即安全連接成功建立狀態(tài)。用函數(shù)LinkState描述車載與地面安全層被期望到達(dá)的數(shù)據(jù)鏈路打開狀態(tài)[DATA]。

步驟2利用ASK-CTL公式myA SKCTLformula描述到達(dá)該期望狀態(tài)的時(shí)序邏輯。

步驟3利用eval_arc myASKCTLformula狀態(tài)空間查詢語句,驗(yàn)證在其狀態(tài)空間內(nèi)是否存在滿足該性質(zhì)的節(jié)點(diǎn)。

圖9中的驗(yàn)證結(jié)果表明,其狀態(tài)空間內(nèi)存在多個(gè)滿足該性質(zhì)的節(jié)點(diǎn)。即協(xié)議期待的安全連接成功建立狀態(tài)可達(dá),安全連接過程具有可操作性。

圖10為數(shù)據(jù)傳輸過程可操作性驗(yàn)證過程,其驗(yàn)證步驟與安全連接建立過程可操作性屬性驗(yàn)證步驟一致,這里不再贅述。驗(yàn)證結(jié)果表明,安全通信協(xié)議建立安全連接后,最終會(huì)進(jìn)入數(shù)據(jù)傳輸階段,使STP車-地之間的數(shù)據(jù)安全可靠傳輸,因此,滿足此階段的可操作性。

圖10 數(shù)據(jù)傳輸過程可操性驗(yàn)證

安全連接建立過程和數(shù)據(jù)傳輸過程的安全性驗(yàn)證如圖11和圖12所示。驗(yàn)證結(jié)果表明STP安全通信協(xié)議在上述2個(gè)過程中,均滿足功能安全性。即在信道環(huán)境理想的條件下,協(xié)議不會(huì)進(jìn)入非安全狀態(tài),其狀態(tài)空間不存在死節(jié)點(diǎn)。

圖11 安全連接建立過程安全性驗(yàn)證

圖12 數(shù)據(jù)傳輸過程安全性驗(yàn)證

然而上述的驗(yàn)證均是在信道理想狀態(tài),即信道不存在干擾和丟包等情況下的結(jié)果,僅保證安全通協(xié)議自身具有安全功能屬性。因此,為驗(yàn)證協(xié)議在非理想信道環(huán)境下也能保證STP車-地間通信系統(tǒng)的安全性,本文在圖4所示的信道子模型內(nèi)引入一定丟包率,造成了數(shù)據(jù)包在無線信道傳輸過程中的丟失現(xiàn)象。在此基礎(chǔ)上,本文再次驗(yàn)證了上述2個(gè)過程的安全性,驗(yàn)證結(jié)果如圖13所示。結(jié)果中的“false”表明,此時(shí)協(xié)議不再滿足連接建立過程的安全性。又通過狀態(tài)空間可達(dá)樹和CPN ML語句:OutArcs5=[],得出狀態(tài)節(jié)點(diǎn)5為“死節(jié)點(diǎn)”,即協(xié)議非安全狀態(tài)。在節(jié)點(diǎn)4至節(jié)點(diǎn)5的變遷綁定(Binding)中,可以得知Trans=FALSE,由于信道的丟包現(xiàn)象,造成安全連接建立過程的連接數(shù)據(jù)包傳輸失敗,出現(xiàn)了非安全狀態(tài)。數(shù)據(jù)傳輸過程的非安全狀態(tài)節(jié)點(diǎn)出現(xiàn)原因與上述同理。由此可見,在不包含連接超時(shí)計(jì)時(shí)子模型的安全通信協(xié)議中,其安全功能僅能保證系統(tǒng)在理想信道環(huán)境下的安全通信。一旦引入信道丟包率,協(xié)議在連接建立過程便會(huì)出現(xiàn)非安全狀態(tài)。

圖13 非理想信道下協(xié)議安全性驗(yàn)證

為使上述“非安全狀態(tài)”導(dǎo)向“安全狀態(tài)”,即故障導(dǎo)向安全,本文在圖6～圖8現(xiàn)有安全功能基礎(chǔ)上,新增替代變遷TimerClock和Timer,均對(duì)應(yīng)圖6所示計(jì)時(shí)器子模型,并在同樣的非理想信道環(huán)境下,驗(yàn)證改進(jìn)后的安全通信協(xié)議連接建立過程的安全性,其ASK-CTL驗(yàn)證結(jié)果如圖14所示。驗(yàn)證結(jié)果中的“true”值表明新增連接超時(shí)重發(fā)機(jī)制的功能安全性,保證了改進(jìn)后的協(xié)議在安全連接建立階段,即使信道存在丟包現(xiàn)象,導(dǎo)致在一定時(shí)間限度內(nèi)接收不到下一包連接數(shù)據(jù)的通信故障狀態(tài)下,也能夠?qū)虬踩珎?cè),從而提高了STP車-地之間通信的安全性和可靠性。

圖14 故障導(dǎo)向安全性驗(yàn)證

4 結(jié)束語

本文依據(jù)歐標(biāo)EN50159,在現(xiàn)有成熟ETCS安全通信協(xié)議EuroRadio安全功能的基礎(chǔ)上,新增雙序號(hào)時(shí)間戳、連接超時(shí)重發(fā)和故障導(dǎo)向安全防護(hù)機(jī)制,設(shè)計(jì)了一個(gè)適用于STP車-地之間通信的安全協(xié)議。利用層次Petri網(wǎng)(CPN)對(duì)該協(xié)議建立模型,通過ASK-CTL時(shí)序邏輯對(duì)協(xié)議進(jìn)行形式化驗(yàn)證。仿真結(jié)果表明,無論是在信道理想情況還是在有一定信道干擾條件下,該通信協(xié)議均具有功能安全性且其安全功能完整。后續(xù)工作將在本文Petri模型的基礎(chǔ)上添加時(shí)間元素,即模型時(shí)間戳,并對(duì)所設(shè)計(jì)的STP安全通信協(xié)議的時(shí)間性能做進(jìn)一步仿真分析。