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

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

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

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

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

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

1 理論背景

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.3 模型死鎖活鎖檢驗

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

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

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

2.4 模型一致性屬性檢驗

對于協(xié)議的動態(tài)行為，一致性屬性可描述不同協(xié)議場景間的時序邏輯［10］，本文對安全通信協(xié)議的2類一致性屬性進行檢驗。

1）第1類：存在一致性屬性

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

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

2）第2類：前向強制一致性屬性

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

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

3 實例應(yīng)用

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

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

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

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

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

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

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

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

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

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

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

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

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

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

表2 CPN模型的架構(gòu)層模型中的符號說明

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

3.4 CPN模型的檢驗

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

（1）屬性1：死鎖。

（2）屬性2：活鎖。

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

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

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

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

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

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

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

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

（1）屬性1和屬性2均滿足。

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

（3）屬性4 不滿足，錯誤路徑與屬性3 中描述的錯誤路徑相同。

（4）屬性5 不滿足，安全服務(wù)用戶A 會收到下層的斷開連接指示。

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

4 結(jié) 語

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