STP安全通信協(xié)議設計與形式化驗證

李 堃,張雪松

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

0 概述

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

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

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

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

表1 常見威脅-防御矩陣

圖1 STP車-地無線通信系統(tǒng)結構

1.1 序列號

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

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

1.2 超時檢測

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

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

1.3 源和目的標識

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

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

1.4 認證機制

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

1.5 安全碼

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

圖6 車載安全層模型

圖7 地面設備安全層模型

圖8 安全層計時器模型

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

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

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

3.1 ASK-CTL相關定義

計算樹時序邏輯(Computational Tree Logic,CTL)是一種典型的分支時序邏輯,是被作為描述有限狀態(tài)系統(tǒng)的一種聲明語言[15]。在描述系統(tǒng)狀態(tài)轉換的性質方面,CTL具有很強的規(guī)范描述邏輯。它用時態(tài)算子描述沿計算路徑的狀態(tài)變化,用路徑算子解釋時間分支性質[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)

為構造復雜的系統(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):表示對于所有路徑,在有限步內使A成立;

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

3.2 形式化驗證

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

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

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

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

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

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

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

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

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

圖10 數據傳輸過程可操性驗證

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

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

圖12 數據傳輸過程安全性驗證

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

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

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

圖14 故障導向安全性驗證

4 結束語

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