張 巖，楊 磊，曾湘毅，孫文橋，劉啟鋼

（1.中國(guó)鐵道科學(xué)研究院集團(tuán)有限公司 運(yùn)輸及經(jīng)濟(jì)研究所，北京 100081；2.中國(guó)鐵道科學(xué)研究院集團(tuán)有限公司 鐵道科學(xué)技術(shù)研究發(fā)展中心，北京 100081；3.中國(guó)鐵路南寧局集團(tuán)有限公司 柳州車(chē)站，廣西 柳州 545007）

安全苛求系統(tǒng)直接關(guān)系到人員的生命、大宗財(cái)產(chǎn)或環(huán)境的安全［1-4］，通常需要采用安全通信協(xié)議確保系統(tǒng)中各通信子系統(tǒng)間實(shí)時(shí)可靠的進(jìn)行通信。模型檢驗(yàn)方法可在協(xié)議規(guī)范設(shè)計(jì)初期及時(shí)徹底檢驗(yàn)協(xié)議規(guī)范的死鎖、活鎖和屬性缺陷，解決開(kāi)發(fā)成本浪費(fèi)和無(wú)法做到完備測(cè)試的問(wèn)題。復(fù)雜系統(tǒng)的模型檢驗(yàn)工作都不可避免地要解決模型狀態(tài)空間爆炸問(wèn)題，解決方法通常是對(duì)系統(tǒng)進(jìn)行抽象。汪洋等［5］提出了先運(yùn)用軟件體系結(jié)構(gòu)方法獲得系統(tǒng)抽象，之后利用模型檢驗(yàn)工具SPIN 對(duì)抽象的模型進(jìn)行檢驗(yàn)，但對(duì)系統(tǒng)進(jìn)行深入抽象難免漏掉一些關(guān)鍵細(xì)節(jié)，使檢驗(yàn)進(jìn)行得不夠精確。

SCH?FER 等［6］將描述對(duì)象行為特性的統(tǒng)一建模語(yǔ)言（Unified Modeling Language，UML）［7］狀態(tài)圖模型轉(zhuǎn)化為Promela 模型，將描述對(duì)象間動(dòng)態(tài)交互關(guān)系的UML 順序圖模型轉(zhuǎn)化為L(zhǎng)TL 公式，最后利用SPIN 進(jìn)行檢驗(yàn)。但半形式化的UML 狀態(tài)圖至Promela 模型的轉(zhuǎn)換存在多種方式，容易受設(shè)計(jì)者主觀(guān)因素影響而產(chǎn)生歧義，導(dǎo)致網(wǎng)絡(luò)協(xié)議的仿真模型與檢驗(yàn)、測(cè)試模型不統(tǒng)一。OUZZIF等［8］通過(guò)狀態(tài)圖模型轉(zhuǎn)化生成的Promela 模型的每個(gè)狀態(tài)下都可以接收任何輸入，但對(duì)某些輸入進(jìn)行空動(dòng)作時(shí)，這樣的不完全提取會(huì)產(chǎn)生不必要多余狀態(tài)，增加模型狀態(tài)空間的體積。

形式化語(yǔ)言接口自動(dòng)機(jī)網(wǎng)絡(luò)（Interface Au?tomata Network，IAN）能夠假設(shè)環(huán)境，不要求輸入使能，可以用來(lái)檢驗(yàn)環(huán)境假設(shè)的錯(cuò)誤［9］。IAN將模塊與環(huán)境之間具有共享接口、但對(duì)環(huán)境的假設(shè)存在矛盾的組合狀態(tài)稱(chēng)為非法狀態(tài)［10-11］。著色Petri網(wǎng)（Colored Petri Net，CPN）是1 種形式化建模語(yǔ)言［12-14］，其工具CPN Tools 可對(duì)CPN 模型進(jìn)行調(diào)試、仿真執(zhí)行和模型檢驗(yàn)，并利用計(jì)算樹(shù)邏輯（Computation Tree Logic，CTL）的檢驗(yàn)擴(kuò)展語(yǔ)言ASK-CTL進(jìn)行模型檢驗(yàn)［15］。

本文提出1 種基于協(xié)議固有層次對(duì)安全通信協(xié)議規(guī)范進(jìn)行模型檢驗(yàn)的方法，按照協(xié)議固有層次用IAN 分層描述復(fù)雜安全通信協(xié)議規(guī)范，建立轉(zhuǎn)化規(guī)則將協(xié)議的IAN 模型轉(zhuǎn)化為CPN 模型，用CPN Tools 檢驗(yàn)出協(xié)議模型中的死鎖和活鎖，從而驗(yàn)證抽象模型的正確性，并檢驗(yàn)協(xié)議模型是否滿(mǎn)足ASK-CTL 描述的各種存在一致性屬性和前向強(qiáng)制一致性屬性。

1 理論背景

1.1 安全通信協(xié)議的分層結(jié)構(gòu)

安全苛求系統(tǒng)通常以網(wǎng)絡(luò)協(xié)議分層作為系統(tǒng)網(wǎng)絡(luò)體系結(jié)構(gòu)的主要方法，安全通信協(xié)議分層后，可以使各層之間相互獨(dú)立，增加靈活性。在同一個(gè)通信實(shí)體上，當(dāng)前層模塊使用下層協(xié)議的服務(wù)向上層協(xié)議提供服務(wù)。同一實(shí)體中相鄰2 層的模塊以服務(wù)訪(fǎng)問(wèn)點(diǎn)（Service Access Point，SAP）作為消息接口，通過(guò)服務(wù)數(shù)據(jù)單元（Service Data Unit，SDU）進(jìn)行消息交互，實(shí)現(xiàn)服務(wù)請(qǐng)求和服務(wù)提供。相同層次上通信雙方的模塊間利用協(xié)議數(shù)據(jù)單元（Protocol Data Unit，PDU）進(jìn)行消息傳輸［16］。

1.2 接口自動(dòng)機(jī)網(wǎng)絡(luò)理論

接口自動(dòng)機(jī)（Interface Automata，IA）是對(duì)系統(tǒng)規(guī)范進(jìn)行建模和分析的工具。IA 規(guī)定當(dāng)前狀態(tài)不可接收的輸入為非法輸入［10］。IA 是1 個(gè)六元組，即

式中：P為1 個(gè)接口自動(dòng)機(jī)；VP為狀態(tài)集，狀態(tài)vi∈VP（0≤i≤|VP|）；VInitP為 初 始 狀 態(tài) 集，VInitP?VP，|VInitP|≤1；當(dāng)VInitP=?時(shí)，P=?；AIP，AOP和AHP分別為輸入、輸出和內(nèi)部動(dòng)作集，AIP∩AOP=AIP∩AHP=AOP∩AHP=?；顯然可以用AP=AIP∪AOP∪AHP表 示P的 全 部 動(dòng) 作 集；ΓP?VP×AP×VP為所有轉(zhuǎn)換的集合。

任取動(dòng)作a∈AP，狀態(tài)v，v'?VP，根據(jù)動(dòng)作類(lèi)型的不同，(v，a，v')可為輸入轉(zhuǎn)換、輸出轉(zhuǎn)換或內(nèi)部轉(zhuǎn)換。

任取狀態(tài)v?VP，對(duì)于動(dòng)作a∈AIP，如果存在狀態(tài)v'?VP使得轉(zhuǎn)換(v，a，v')∈ΓP，那么稱(chēng)a在狀態(tài)v上是可激活的，即輸入使能［10］。

多個(gè)接口自動(dòng)機(jī)可組成1 個(gè)接口自動(dòng)機(jī)網(wǎng)絡(luò)。1個(gè)接口自動(dòng)機(jī)網(wǎng)絡(luò)（Interface Automata Network，IAN）中，N是二元組

式中：M={P1，P2，…，Pn}為可組合的IA集；AS=｛shared（Pi，Pj）｝（1≤i，j≤n，i≠j）為所有的共享的動(dòng)作集。

2 安全通信協(xié)議規(guī)范分層模型檢驗(yàn)方法

安全通信協(xié)議規(guī)范的形式化建模與檢驗(yàn)方法包括分層建模、模型轉(zhuǎn)化、死鎖和活鎖檢驗(yàn)以及一致性屬性檢驗(yàn)4個(gè)步驟。根據(jù)協(xié)議的層次化結(jié)構(gòu)，選擇IAN 對(duì)協(xié)議進(jìn)行分層建模，將模型轉(zhuǎn)化為CPN模型，檢驗(yàn)?zāi)Ｐ椭袩o(wú)死鎖和活鎖后，利用ASKCTL公式對(duì)協(xié)議一致性屬性進(jìn)行描述并檢驗(yàn)。

2.1 安全通信協(xié)議規(guī)范分層建模方法

為了避免狀態(tài)空間爆炸，使模型檢驗(yàn)更有針對(duì)性、建模思路更清晰、模型復(fù)雜性更低，基于分層結(jié)構(gòu)，對(duì)協(xié)議目標(biāo)層模塊進(jìn)行模型檢驗(yàn)，需要在上層建立通信雙方測(cè)試層測(cè)試模塊的模型，在目標(biāo)層建立通信雙方功能模塊的模型，在下層建立協(xié)助層協(xié)助測(cè)試模塊的模型，模型整體結(jié)構(gòu)的示意圖如圖1 所示。圖中：實(shí)線(xiàn)框和虛線(xiàn)框分別代表實(shí)際和抽象的模塊；箭頭表示數(shù)據(jù)交互方向。由圖1 可知：通信雙方各自包含1 個(gè)服務(wù)用戶(hù)模塊和1 個(gè)功能模塊，模塊間通過(guò)服務(wù)訪(fǎng)問(wèn)點(diǎn)SAP 實(shí)現(xiàn)服務(wù)數(shù)據(jù)單元SDU 的交互；傳輸模塊模擬協(xié)議底層數(shù)據(jù)傳輸通道，實(shí)現(xiàn)PDU的傳輸。

圖1 協(xié)議規(guī)范模型整體結(jié)構(gòu)示意圖

選擇適合抽象多模塊復(fù)雜規(guī)范行為的IAN 進(jìn)行建模，需用5 個(gè)IA 分別對(duì)各層的模塊進(jìn)行描述，利用IA 的輸入、輸出動(dòng)作集描述模塊間的各種消息交互，從而構(gòu)成1 個(gè)IAN。為了實(shí)現(xiàn)目標(biāo)層行為的有效模型檢驗(yàn)，目標(biāo)層的模塊需要根據(jù)協(xié)議規(guī)范進(jìn)行詳細(xì)建模，描述協(xié)議所有的狀態(tài)和狀態(tài)間的遷移規(guī)則。在滿(mǎn)足與目標(biāo)層模塊接口列表不變的前提下，對(duì)測(cè)試層和協(xié)助層的狀態(tài)和遷移進(jìn)行深入提取，控制模型整體狀態(tài)空間的體積。

2.2 IAN模型到CPN模型的轉(zhuǎn)化

IAN 模型可映射為分層結(jié)構(gòu)的CPN 模型，成為模型檢驗(yàn)工具CPN Tools 可以檢驗(yàn)的形式化模型，轉(zhuǎn)化規(guī)則見(jiàn)表1?；贗AN 的固有結(jié)構(gòu)，利用包括架構(gòu)層和實(shí)現(xiàn)層的CPN 分層模型對(duì)IAN 進(jìn)行描述。架構(gòu)層只描述所有IA 之間的接口關(guān)系，用替代變遷描述IA，用庫(kù)所描述IA 之間的接口。實(shí)現(xiàn)層通過(guò)對(duì)替代變遷的詳細(xì)描述實(shí)現(xiàn)對(duì)IA 內(nèi)部狀態(tài)、動(dòng)作和轉(zhuǎn)換的建模，通過(guò)對(duì)具有I/O 標(biāo)識(shí)的庫(kù)所的詳細(xì)描述實(shí)現(xiàn)對(duì)接口消息傳遞過(guò)程的建模。

表1 IAN模型到CPN模型的轉(zhuǎn)化規(guī)則

2.3 模型死鎖活鎖檢驗(yàn)

協(xié)議執(zhí)行過(guò)程中可能存在死鎖和活鎖2 種錯(cuò)誤，產(chǎn)生死鎖和活鎖的原因可能是安全通信協(xié)議規(guī)范本身錯(cuò)誤或建模錯(cuò)誤。建模正確是檢驗(yàn)的基礎(chǔ)，在檢驗(yàn)IAN 行為屬性前，需要去除建模錯(cuò)誤導(dǎo)致的死鎖和活鎖，然后通過(guò)模型檢驗(yàn)的方法檢查出安全通信協(xié)議規(guī)范的死鎖和活鎖。

IAN 中的非法狀態(tài)會(huì)導(dǎo)致安全通信協(xié)議死鎖。對(duì)于接口自動(dòng)機(jī)網(wǎng)絡(luò)N，任取2 個(gè)接口自動(dòng)機(jī)Pi∈N，Pj∈N，當(dāng)Pi對(duì)Pj有輸出動(dòng)作、Pj的當(dāng)前狀態(tài)無(wú)對(duì)應(yīng)輸入動(dòng)作，即當(dāng)前狀態(tài)無(wú)法激活時(shí)，Pj進(jìn)入非法狀態(tài)，模型無(wú)法繼續(xù)執(zhí)行，產(chǎn)生死鎖。與I/O 自動(dòng)機(jī)不同，IA 不保證一定滿(mǎn)足輸入使能，會(huì)導(dǎo)致IAN 可真實(shí)描述安全通信協(xié)議規(guī)范中的死鎖。死鎖檢驗(yàn)方法是利用CPN ToolS 工具的ListDead?Markings（·）函數(shù)搜索CPN 模型中存在的死標(biāo)記（Dead Markings）［15］，如果CPN 模型的死標(biāo)記集合為空或者全部死標(biāo)記被標(biāo)注為正常停止?fàn)顟B(tài)，則模型中無(wú)死鎖，否則存在死鎖。

活鎖指協(xié)議的CPN 模型陷入局部無(wú)限循環(huán)。本文給出的活鎖模型檢驗(yàn)方法是：首先檢驗(yàn)?zāi)Ｐ偷膹?qiáng)連通圖［15］是否與模型狀態(tài)空間同構(gòu)，兩者同構(gòu)且無(wú)自循環(huán)的節(jié)點(diǎn)可保證CPN 模型無(wú)活鎖；然后判斷CPN模型的狀態(tài)空間中是否存在節(jié)點(diǎn)數(shù)大于1的強(qiáng)連通分量或自循環(huán)節(jié)點(diǎn)，如果不存在則CPN模型無(wú)活鎖；反之還需要繼續(xù)判斷條件“模型狀態(tài)空間所有停止分量［15］均僅含1 個(gè)節(jié)點(diǎn)且不存在弧”，條件滿(mǎn)足則CPN 模型無(wú)活鎖，條件不滿(mǎn)足則CPN模型存在活鎖。

2.4 模型一致性屬性檢驗(yàn)

對(duì)于協(xié)議的動(dòng)態(tài)行為，一致性屬性可描述不同協(xié)議場(chǎng)景間的時(shí)序邏輯［10］，本文對(duì)安全通信協(xié)議的2類(lèi)一致性屬性進(jìn)行檢驗(yàn)。

1）第1類(lèi)：存在一致性屬性

用于檢驗(yàn)協(xié)議模型狀態(tài)空間所有行為中是否包含特定場(chǎng)景D，或者協(xié)議模型狀態(tài)空間所有行為的集合一定不包含場(chǎng)景D。對(duì)該類(lèi)一致性屬性檢驗(yàn)的ASK-CTL 公式見(jiàn)式（1），表示在模型狀態(tài)空間M上，從初始狀態(tài)s0開(kāi)始，場(chǎng)景D可能發(fā)生或場(chǎng)景D永遠(yuǎn)不會(huì)發(fā)生。

式中：函數(shù)Pos（·）為使括號(hào)中單項(xiàng)式成立的未來(lái)某個(gè)狀態(tài)；?表示邏輯“非”，函數(shù)Inv（·）為使括號(hào)中單項(xiàng)式成立的未來(lái)所有狀態(tài)。

2）第2類(lèi)：前向強(qiáng)制一致性屬性

用于檢驗(yàn)在協(xié)議執(zhí)行過(guò)程中，當(dāng)條件場(chǎng)景D1出現(xiàn)后，場(chǎng)景D2一定會(huì)隨之在協(xié)議的后續(xù)行為中發(fā)生。對(duì)該類(lèi)一致性屬性檢驗(yàn)的ASK-CTL公式見(jiàn)式（2），表示在模型狀態(tài)空間M上，從初始狀態(tài)s0開(kāi)始，場(chǎng)景D1的發(fā)生一定會(huì)引起場(chǎng)景D2的發(fā)生。

式中：函數(shù)Ev（·）為存在使括號(hào)中多項(xiàng)式成立的狀態(tài)；符號(hào)→表示“引起”。

3 實(shí)例應(yīng)用

3.1 ETCS安全通信協(xié)議規(guī)范描述

按照鐵路安全苛求系統(tǒng)安全相關(guān)通信標(biāo)準(zhǔn)IEC 62280-2的規(guī)定［17］，不可信傳輸通道上必須建立具備安全傳輸功能的安全通信協(xié)議，歐洲列車(chē)運(yùn)行控制系統(tǒng)（European Railway Control System，ETCS）的安全通信協(xié)議用來(lái)確保高速列車(chē)車(chē)載設(shè)備和地面無(wú)線(xiàn)閉塞中心（Radio Block Center，RBC）之間的位置、運(yùn)行權(quán)限（Movement Author?ity，MA）等報(bào)文的實(shí)時(shí)安全傳輸，協(xié)議規(guī)范［18］給出了安全通信協(xié)議的分層結(jié)構(gòu)，如圖2 所示。圖中：方框表示模塊，橢圓框表示服務(wù)接入點(diǎn)。

圖2 ETCS安全協(xié)議分層結(jié)構(gòu)

安全通信協(xié)議的分層結(jié)構(gòu)描述了安全服務(wù)用戶(hù)、安全功能模塊和傳輸功能模塊之間的交互關(guān)系，按照協(xié)議規(guī)范的規(guī)定，安全服務(wù)用戶(hù)通過(guò)安全功能模塊發(fā)送和接收高優(yōu)先級(jí)或普通數(shù)據(jù)，安全功能模塊提供安全連接建立、安全數(shù)據(jù)傳輸?shù)陌踩?wù)，其中安全數(shù)據(jù)傳輸保證數(shù)據(jù)的完整性和真實(shí)性。安全功能模塊向上層報(bào)告發(fā)生在本層或底層的錯(cuò)誤。安全功能模塊作為安全服務(wù)提供者，同時(shí)也是傳輸服務(wù)使用者。傳輸功能模塊需要向安全功能模塊提供傳輸層連接的建立和釋放、可靠數(shù)據(jù)傳輸、透明的數(shù)據(jù)傳輸和高優(yōu)先級(jí)數(shù)據(jù)傳輸?shù)确?wù)，各層具體功能詳見(jiàn)歐洲無(wú)線(xiàn)通信功能接口規(guī)范［18］。

3.2 協(xié)議規(guī)范層次結(jié)構(gòu)IAN模型的建立

根據(jù)安全通信協(xié)議規(guī)范的分層結(jié)構(gòu)抽象出1 個(gè)IAN 模型，其中包含5 個(gè)IA 模型分別為P1，P2，…，P5。協(xié)議測(cè)試層的IAN 模型如圖3 所示。圖中：方形表示接口；圓形表示狀態(tài)；弧線(xiàn)箭頭表示狀態(tài)遷移的方向；方形旁邊的箭頭表示輸入/輸出；P1模型描述測(cè)試層連接發(fā)起方安全服務(wù)用戶(hù)A，主要用來(lái)模擬連接發(fā)起方安全服務(wù)用戶(hù)向安全功能模塊發(fā)送建立、刪除連接請(qǐng)求等SDU；P5模型描述測(cè)試層連接跟隨方安全服務(wù)用戶(hù)B，主要用來(lái)模擬連接跟隨方安全服務(wù)用戶(hù)從安全功能模塊接收建立、刪除連接指示等SDU。

最低層協(xié)助層傳輸模塊的P3模型如圖4 所示。圖中：字母“S”表示連接發(fā)起方；字母“F”表示連接跟隨方；括號(hào)內(nèi)的字母“u”表示傳輸層將上層安全功能模塊的第1 認(rèn)證、第2 認(rèn)證、認(rèn)證應(yīng)答等PDU 轉(zhuǎn)發(fā)給對(duì)方安全功能模塊；P3模型用來(lái)描述整個(gè)傳輸層，模擬所有安全功能模塊可能使用的功能，且需要提取出所有與目標(biāo)層相關(guān)的狀態(tài)，其他狀態(tài)忽略，因此P3模型的主要功能是將從1端安全功能模塊接收的消息傳輸至另1端安全功能模塊。

安全功能模塊的有限狀態(tài)機(jī)模型如圖5 所示，描述了安全功能模塊內(nèi)部的狀態(tài)轉(zhuǎn)換行為。安全功能模塊包括空閑、等待傳輸連接、等待認(rèn)證應(yīng)答等6 個(gè)狀態(tài)，任意2 個(gè)狀態(tài)之間為1 個(gè)狀態(tài)轉(zhuǎn)換，狀態(tài)轉(zhuǎn)換上符號(hào)“/”的前面表示轉(zhuǎn)換條件，后面表示動(dòng)作，括號(hào)中的第1 認(rèn)證、第2 認(rèn)證、認(rèn)證應(yīng)答等為安全功能模塊的PDU。安全功能模塊通過(guò)進(jìn)行狀態(tài)轉(zhuǎn)換，執(zhí)行一系列動(dòng)作，完成連接發(fā)起方和連接跟隨方安全功能模塊PDU 的交互，實(shí)現(xiàn)連接的建立和刪除過(guò)程。可從圖3中安全功能模塊的有限狀態(tài)機(jī)模型獲得連接發(fā)起方、連接跟隨方目標(biāo)層安全功能模塊的P2模型和P4模型。為了減小模型狀態(tài)空間，安全功能模塊的IA 模型按照連接發(fā)起方與跟隨方分別建立，2個(gè)模塊的IA模型根據(jù)連接發(fā)起與跟隨的不同功能，具有不同的功能和狀態(tài)。基于安全功能模塊的有限狀態(tài)機(jī)模型，根據(jù)連接發(fā)起方與跟隨方的不同來(lái)分別提取出P2模型和P4模型，這樣每個(gè)IA 模型的狀態(tài)數(shù)都可以成倍減小，從而避免狀態(tài)空間爆炸。

圖3 協(xié)議規(guī)范測(cè)試層的P1模型和P5模型

圖4 協(xié)議規(guī)范協(xié)助層的P3模型

圖5 安全功能模塊的有限狀態(tài)機(jī)模型

協(xié)議模型檢驗(yàn)?zāi)康氖前l(fā)現(xiàn)協(xié)議中的設(shè)計(jì)缺陷，或檢驗(yàn)協(xié)議是否滿(mǎn)足一些屬性，必須將所有不利的條件事先都估計(jì)到，狀態(tài)遷移也應(yīng)該反應(yīng)所有異常情況。如可以模擬安全功能模塊在等待認(rèn)證應(yīng)答時(shí)隨機(jī)收到錯(cuò)誤的對(duì)等實(shí)體的第2 認(rèn)證消息后，向傳輸功能層發(fā)送斷開(kāi)連接請(qǐng)求，準(zhǔn)備進(jìn)入空閑狀態(tài)。

3.3 IAN模型到CPN模型的轉(zhuǎn)換

利用給出的IAN 模型到CPN 模型的轉(zhuǎn)化規(guī)則（表1），可獲得協(xié)議規(guī)范的CPN架構(gòu)層模型，如圖6 所示，圖6 中符號(hào)的說(shuō)明見(jiàn)表2。CPN 架構(gòu)層模型包括安全服務(wù)用戶(hù)A、連接發(fā)起方安全功能模塊、傳輸模塊、連接跟隨方安全功能模塊、安全服務(wù)用戶(hù)B 等5 個(gè)替代變遷，分別對(duì)應(yīng)IAN 中的5 個(gè)IA。有信息交互的替代變遷之間均用向下接口和向上接口庫(kù)所保存協(xié)議上層至下層和下層至上層的輸入、輸出接口消息。利用IAN 模型到CPN 模型的轉(zhuǎn)化規(guī)則可獲得協(xié)議規(guī)范的CPN 實(shí)現(xiàn)層模型，用5個(gè)頁(yè)面詳細(xì)實(shí)現(xiàn)各替代變遷。

表2 CPN模型的架構(gòu)層模型中的符號(hào)說(shuō)明

圖6 協(xié)議規(guī)范CPN模型的架構(gòu)層模型

3.4 CPN模型的檢驗(yàn)

模型檢驗(yàn)可檢驗(yàn)協(xié)議規(guī)范是否存在死鎖、活鎖或滿(mǎn)足一些安全行為屬性，并找出反例路徑。需要進(jìn)行檢驗(yàn)的5條屬性的描述如下。

（1）屬性1：死鎖。

（2）屬性2：活鎖。

（3）屬性3：前向強(qiáng)制一致性。連接發(fā)送方安全服務(wù)用戶(hù)A 發(fā)送建立連接請(qǐng)求后一定可收到連接確認(rèn)。根據(jù)式（2），該屬性可用式（3）進(jìn)行描述。

式中：場(chǎng)景SaUserA_SaConnReq 為安全服務(wù)用戶(hù)A 處于輸出連接建立請(qǐng)求狀態(tài)；場(chǎng)景SaUserA_SaConnConf 為安全服務(wù)用戶(hù)A 處于輸入連接建立確認(rèn)狀態(tài)。

（4）屬性4：前向強(qiáng)制一致性。連接發(fā)起方安全服務(wù)用戶(hù)A 輸出SaHpDataReq 服務(wù)原語(yǔ)后一定會(huì)輸出THpDataReq，且本屬性同樣適用于連接跟隨方。根據(jù)式（2），該屬性可用式（4）進(jìn)行描述。

式中：場(chǎng)景SaUserA_SaHpDataReq 為安全服務(wù)用戶(hù)A 處于輸出高優(yōu)先級(jí)數(shù)據(jù)請(qǐng)求狀態(tài)；場(chǎng)景SaLA_ThpDataReq 為安全功能模塊A 處于輸出高優(yōu)先級(jí)數(shù)據(jù)請(qǐng)求狀態(tài)。

（5）屬性5：存在一致性。安全服務(wù)用戶(hù)A 不會(huì)收到下層的斷開(kāi)連接指示，且本屬性同樣適用于連接跟隨方。屬性5為式（1）描述的第1類(lèi)存在一致性屬性，可用式（5）進(jìn)行描述。

式中：場(chǎng)景SaUserA_SaDiscInd 為安全服務(wù)用戶(hù)處于收到斷開(kāi)連接指示狀態(tài)。

3.5 CPN模型檢驗(yàn)結(jié)果及分析

利用版本號(hào)為Version 4.0.1 的CPN Tools 對(duì)建立的CPN 模型進(jìn)行模型檢驗(yàn)，CPN Tools 可在100 s 內(nèi)生成該CPN 模型的狀態(tài)空間，未出現(xiàn)狀態(tài)空間爆炸的情況，模型檢驗(yàn)可正常實(shí)施，檢驗(yàn)結(jié)果及分析如下。

（1）屬性1和屬性2均滿(mǎn)足。

（2）屬性3 不滿(mǎn)足，通過(guò)分析CPN Tools 給出的模型狀態(tài)空間中的反例路徑，安全功能模塊A錯(cuò)誤路徑之一是：空閑狀態(tài)→建立連接請(qǐng)求狀態(tài)→斷開(kāi)連接狀態(tài)→空閑狀態(tài)。當(dāng)安全功能模塊A 收到上層錯(cuò)誤格式的連接建立請(qǐng)求服務(wù)原語(yǔ)后，連接建立過(guò)程失敗。

（3）屬性4 不滿(mǎn)足，錯(cuò)誤路徑與屬性3 中描述的錯(cuò)誤路徑相同。

（4）屬性5 不滿(mǎn)足，安全服務(wù)用戶(hù)A 會(huì)收到下層的斷開(kāi)連接指示。

由此可知：安全功能模塊規(guī)范不存在死鎖和活鎖，可處于正常停止?fàn)顟B(tài)且不會(huì)陷入死循環(huán)，安全功能模塊流程設(shè)計(jì)合理；安全功能模塊的連接建立過(guò)程可能存在不成功的情況，主要原因是底層無(wú)線(xiàn)通信鏈路可能存在丟包或延時(shí)等情況，因此列車(chē)控制系統(tǒng)應(yīng)用層應(yīng)具備連接功能失效的響應(yīng)處理流程；由于數(shù)據(jù)傳輸過(guò)程中無(wú)線(xiàn)通信存在中斷的可能，安全功能模塊可能存在高優(yōu)先級(jí)數(shù)據(jù)無(wú)法傳輸和車(chē)地間通信連接斷開(kāi)的情況，因此車(chē)載設(shè)備應(yīng)具備相應(yīng)的故障導(dǎo)向安全的防護(hù)功能。

4 結(jié) 語(yǔ)

針對(duì)安全通信協(xié)議的多層復(fù)雜結(jié)構(gòu)，利用IAN 適合對(duì)復(fù)雜多模塊模型進(jìn)行抽象的特點(diǎn)，采用分而治之的辦法，將大規(guī)模協(xié)議按照其固有層次分解成若干個(gè)模塊，每次選擇1個(gè)模塊進(jìn)行模型檢驗(yàn)，每次檢驗(yàn)只關(guān)注協(xié)議某一層內(nèi)的相關(guān)邏輯，對(duì)關(guān)鍵層進(jìn)行詳細(xì)描述，在保證關(guān)鍵層接口不變和保留所有關(guān)鍵細(xì)節(jié)的基礎(chǔ)上，對(duì)輔助模塊進(jìn)行深入提取，減小了檢驗(yàn)?zāi)Ｐ偷膹?fù)雜度，避免了模型狀態(tài)空間爆炸。以ETCS安全通信協(xié)議的安全功能模塊規(guī)范為例，檢驗(yàn)了協(xié)議規(guī)范的死鎖、活鎖和存在一致性、前向強(qiáng)制一致性2 類(lèi)屬性，發(fā)現(xiàn)安全功能模塊規(guī)范不存在死鎖和活鎖，但存在安全功能模塊的連接建立過(guò)程不成功、高優(yōu)先級(jí)數(shù)據(jù)無(wú)法傳輸和車(chē)地間通信連接斷開(kāi)的情況。表明利用分層方法提取協(xié)議的抽象IAN 模型，通過(guò)統(tǒng)一轉(zhuǎn)化規(guī)則轉(zhuǎn)化為CPN模型并進(jìn)行檢驗(yàn)，是1種解決協(xié)議設(shè)計(jì)過(guò)程中的屬性檢驗(yàn)問(wèn)題的有效方式。