李 堃,張雪松

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

0 概述

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

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

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

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

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

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

1.2 超時檢測

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

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

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

STP車-地通信系統(tǒng)是一個多端通信系統(tǒng)。因為在大型編組站內(nèi),通常會有多臺地面設(shè)備控制不同站場內(nèi)的多臺調(diào)車機車同時作業(yè),所以在使用所接收到的信息之前,需要用合適的方法來檢測信息的來源。

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

1.4 認證機制

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

1.5 安全碼

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖6 車載安全層模型

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

圖8 安全層計時器模型

3 基于ASK-CTL的形式化驗證

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

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

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

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

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)時序邏輯表達式,ASK-CTL還有以下擴展操作符:

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

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

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

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

3.2 形式化驗證

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

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

圖9 安全連接建立過程可操作性驗證

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

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

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

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

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

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

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

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

圖11 安全連接建立過程安全性驗證

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

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

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

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

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

4 結(jié)束語

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