王恪銘 ，王 霞 ，程 鵬 ，劉 寧 ，張傳東

（1.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院，四川 成都 611756；2.西南交通大學(xué)系統(tǒng)可信性自動(dòng)驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室，四川 成都 610031；3.西南交通大學(xué)唐山研究生院，河北 唐山 063000；4.北京和利時(shí)系統(tǒng)工程有限公司，北京 100176）

車站聯(lián)鎖系統(tǒng)是典型的安全苛求系統(tǒng)，保障著車站內(nèi)的行車效率與安全，該系統(tǒng)內(nèi)在的行為缺陷會(huì)對(duì)車站的日常運(yùn)營造成巨大的損失[1].此外，車站聯(lián)鎖系統(tǒng)由聯(lián)鎖表驅(qū)動(dòng)，驗(yàn)證數(shù)據(jù)的正確性對(duì)于該系統(tǒng)的安全運(yùn)行也至關(guān)重要.

形式化方法是提高系統(tǒng)安全可靠性的一種有效方法，當(dāng)系統(tǒng)的安全完整性等級(jí)達(dá)到SIL3級(jí)及以上時(shí)，IEC 61508[2]推薦使用該方法進(jìn)行系統(tǒng)驗(yàn)證.形式化方法在車站聯(lián)鎖系統(tǒng)中也有應(yīng)用，如有：文獻(xiàn)[3]使用形式化建模工具UPPAAL建立了聯(lián)鎖系統(tǒng)的時(shí)間自動(dòng)機(jī)模型，并對(duì)安全相關(guān)屬性進(jìn)行了驗(yàn)證；文獻(xiàn)[4]建立了滿足序列釋放特性的車站網(wǎng)絡(luò)聯(lián)鎖系統(tǒng)模型，基于有界模型檢驗(yàn)及歸納推理方法，使用SMT（satisfiability modulo theories）求解器進(jìn)行了驗(yàn)證.

以上研究中都忽略了對(duì)聯(lián)鎖數(shù)據(jù)進(jìn)行確認(rèn)，近年來，基于數(shù)據(jù)視角的系統(tǒng)安全性逐漸被重視，如文獻(xiàn)[5]提出了一種用反例引導(dǎo)抽象精化范式的方法對(duì)車站聯(lián)鎖數(shù)據(jù)進(jìn)行確認(rèn)，文獻(xiàn)[6]中使用ProB證明器確認(rèn)了聯(lián)鎖數(shù)據(jù).

綜上所述，目前大多數(shù)聯(lián)鎖數(shù)據(jù)驗(yàn)證研究使用的都是模型檢驗(yàn)方法，針對(duì)特定對(duì)象構(gòu)建專門的模型.這些方法忽略了不同車站聯(lián)鎖數(shù)據(jù)確認(rèn)的通用性.且形式化驗(yàn)證方法可分為模型檢驗(yàn)與定理證明兩種，后者彌補(bǔ)了模型檢驗(yàn)方法只能處理有限狀態(tài)空間的缺陷，Event-B語言是其中的典型代表，在該語言的支持平臺(tái)RODIN中，模型檢驗(yàn)與定理證明兩種方法得到了有機(jī)結(jié)合[7].基于此，本文分析了聯(lián)鎖系統(tǒng)通用功能需求規(guī)范的形式化建模流程，使用Event-B語言描述，基于逐層精化策略建立了一個(gè)通用的聯(lián)鎖系統(tǒng)行為模型，并結(jié)合車站實(shí)例仿真、驗(yàn)收測試，提出了車站聯(lián)鎖系統(tǒng)行為驗(yàn)證與數(shù)據(jù)確認(rèn)的形式化方法.

1 基于Event-B語言的形式化建模

Event-B是一種使用一階、命題邏輯與集合論作為建模符號(hào)，描述離散系統(tǒng)的建模語言[1].Event-B模型由兩部分組成[1,7]：場景文件（context）和機(jī)器文件（machine），其中場景文件定義了系統(tǒng)的靜態(tài)屬性，包括系統(tǒng)的基本組成對(duì)象以及運(yùn)行時(shí)必須遵循的準(zhǔn)則；機(jī)器文件定義了系統(tǒng)運(yùn)行時(shí)的動(dòng)態(tài)屬性，由變量（variable）、不變式（invariant，運(yùn)行過程中應(yīng)滿足的基本原則）、變體（variant）和事件（event）組成.

1.1 規(guī)范分析

建模之前需要進(jìn)行規(guī)范分析.首先基于國標(biāo)規(guī)范[8]，將通用聯(lián)鎖系統(tǒng)中的各類屬性按照要求分為環(huán)境類、功能類和安全類3類，其中環(huán)境類屬性被用來描述系統(tǒng)中建模的對(duì)象[1]，例如ENV_DG1：軌道區(qū)段分為道岔區(qū)段、無岔區(qū)段；功能屬性描述系統(tǒng)對(duì)象應(yīng)當(dāng)具備的基本功能以及其執(zhí)行條件，例如FUN_SIG1：信號(hào)機(jī)能正常顯示建立進(jìn)路時(shí)應(yīng)當(dāng)顯示的燈色；安全類屬性描述運(yùn)行過程中保障安全苛求標(biāo)準(zhǔn)應(yīng)具備的條件，例如SAF_SIG2：如果區(qū)段故障占用在信號(hào)保持階段時(shí)發(fā)生，需要立即關(guān)閉信號(hào)機(jī)，但不能解鎖進(jìn)路.

事件是系統(tǒng)功能在基于安全類屬性約束場景中的具體表現(xiàn).在分析過程中，要得出各個(gè)功能對(duì)應(yīng)的基本事件及其執(zhí)行條件，分解出復(fù)雜功能的初始化狀態(tài)、基本事件組成集合與執(zhí)行順序，并構(gòu)建該功能的所有場景與安全性約束.以上過程中可使用STAMP（system-theoretic accident model and processes）等安全分析方法，并建議使用UML工具輔助構(gòu)建可視化流程.且由于各屬性與事件流程的對(duì)應(yīng)規(guī)范文本內(nèi)容往往數(shù)倍于系統(tǒng)需求本身，管理難度加大，可使用相應(yīng)的需求管理工具（如RODIN平臺(tái)中的ProR），以保持在修改過程中分析成果與后續(xù)模型的邏輯一致性.

1.2 初始模型

車站聯(lián)鎖系統(tǒng)主要是對(duì)進(jìn)路流程進(jìn)行控制，初始模型設(shè)計(jì)了進(jìn)路的建立與解鎖.對(duì)應(yīng)場景文件中定義了進(jìn)路的抽象集合ROUTE；在機(jī)器文件中包含兩個(gè)事件：建立進(jìn)路lock_route和解鎖進(jìn)路release_route，且定義集合lockedRoute來表示已經(jīng)建立的進(jìn)路，r表示進(jìn)路序號(hào).本文研究的建模過程中，使用了RODIN平臺(tái)中的iUML-B插件，通過建立環(huán)境變量與事件流程UML圖（如圖1所示），直接生成場景文件與機(jī)器文件（如圖2所示），提高建模過程的準(zhǔn)確性及自動(dòng)化程度.

圖1 初始模型中事件的 UMLFig.1 UML diagram for event of initial model

圖2 初始模型中的機(jī)器文件Fig.2 Machine file in initial model

1.3 精化策略

精化策略是指在模型建立過程中，將復(fù)雜的系統(tǒng)功能進(jìn)行層次分解的建模策略.即首先建立初始模型，在初始模型得到實(shí)現(xiàn)且通過證明后，后續(xù)模型擴(kuò)展的場景文件與精化的機(jī)器文件可以繼承已被證明的定理、不變式，在此過程中逐步完善系統(tǒng)功能.本文的精化過程如表1所示.

表1 模型各層精化內(nèi)容Tab.1 Refinement of the model

下文以第1層的Event-B精化模型為例，說明對(duì)象的引入與事件的添加過程.

1.3.1 第 1 層精化模型中的場景文件

定義軌道區(qū)段集合SECTION、列車的抽象集合TRAIN，EXTRA_TRACK、TRACK分別被定義為站外軌道區(qū)段、站內(nèi)軌道區(qū)段，且EXTRA_TRACK?SECTION，TRACK?SECTION.站外軌道區(qū)段與站內(nèi)軌道區(qū)段不能同時(shí)包含同一個(gè)軌道區(qū)段，即有如式（1）所示的公理定義.

用routeTrack表示每一條進(jìn)路中含有的軌道區(qū)段.顯然，各個(gè)軌道區(qū)段可以屬于各個(gè)不同的進(jìn)路，每一個(gè)進(jìn)路區(qū)段也都可以包含有多條不同的軌道區(qū)段，因此routeTrack被定義為

設(shè)routeTrackNum為進(jìn)路中各軌道區(qū)段的連接序號(hào)，屬于ROUTE與軌道區(qū)段有序集合TRACK的全函數(shù)，其中在軌道區(qū)段的有序集合中，使用了不同編號(hào)以表示各個(gè)軌道區(qū)段，軌道區(qū)段與編號(hào)的關(guān)系為單射函數(shù)；進(jìn)路中的軌道區(qū)段數(shù)量用routeTrack-Count表示，屬于ROUTE和整數(shù)間的全函數(shù).

用approachSection表示每條進(jìn)路與其接近區(qū)段的映射關(guān)系：

1.3.2 第 1 層精化模型中的機(jī)器文件

由于加入了軌道區(qū)段，第1層精化模型中的機(jī)器文件新增了以下兩個(gè)變量：變量lockedTrack記錄鎖閉軌道區(qū)段的進(jìn)路，以便在解鎖進(jìn)路時(shí)對(duì)相應(yīng)區(qū)段進(jìn)行解鎖，因此lockedTrack為TRACK與ROUTE之間的二元關(guān)系.進(jìn)路的狀態(tài)只有鎖閉或解鎖狀態(tài)兩類，故將lockedTrack定義為TRACK到ROUTE的部分函數(shù)關(guān)系；變量train_Pos用于記錄站內(nèi)站外所有列車的位置信息，因此有

本層模型中共有11個(gè)事件，以圖3中的事件train_into_route為例說明如下：

圖3 精化模型一中 train_into_route 事件Fig.3 Event of train_into_route in refined model 1

該事件用于實(shí)現(xiàn)車輛由站外區(qū)段駛?cè)胝緝?nèi)，精化擴(kuò)展了初始模型中的事件release_route，事件release_route中對(duì)站內(nèi)區(qū)段鎖閉集合lockedRoute進(jìn)行過定義.當(dāng)進(jìn)路r建立（grd1），且進(jìn)路r的站外起始區(qū)段（比如第1離去區(qū)段）有車占用時(shí)（grd2），滿足觸發(fā)事件train_into_route執(zhí)行的條件，車輛可以由這些區(qū)段駛?cè)胝緝?nèi).該事件執(zhí)行后，進(jìn)路r釋放（act1），且站外區(qū)段恢復(fù)空閑，同時(shí)車輛當(dāng)前位置由站外區(qū)段更新為該進(jìn)路的第1個(gè)站內(nèi)區(qū)段，原站外區(qū)段恢復(fù)空閑（act2）.該事件在之后各層中還將得到精化，如增加車輛初始位置限制，區(qū)分列車與調(diào)車進(jìn)路等.

在事件train_into_route執(zhí)行后，將觸發(fā)執(zhí)行車輛前行事件train_move，并正常解鎖（分段解鎖）道岔、站內(nèi)區(qū)段，直至車輛到達(dá)進(jìn)路r的最末區(qū)段，則進(jìn)路r執(zhí)行結(jié)束.此時(shí)進(jìn)路r雖被釋放，但不滿足重新建立的條件，如該進(jìn)路最末區(qū)段仍被占用，進(jìn)路r仍為非空閑狀態(tài).最終功能實(shí)現(xiàn)可見該模型精化后的最后一層機(jī)器文件M6[9-10].

2 系統(tǒng)屬性驗(yàn)證

2.1 驗(yàn)證屬性的Event-B描述

在場景文件中，集合或常量之間的屬性定義為公理（axiom）.基于第1層精化模型中的場景文件，兩條屬性被定義成如下公理：

1）在任意進(jìn)路，關(guān)系集合routeTrack對(duì)應(yīng)的軌道區(qū)段，也會(huì)存在于routeTrackNum定義域所包含的軌道區(qū)段之中.其Event-B描述對(duì)應(yīng)如下：

式中：符號(hào)?為蘊(yùn)含操作符；dom(?)為定義域操作；?為值域限制操作[7].

2）routeTrack與routeTrackNum不等價(jià).在調(diào)車進(jìn)路當(dāng)中，如果無岔區(qū)段或到發(fā)線股道是最末端的軌道區(qū)段，則在聯(lián)鎖檢查中不需要考慮該區(qū)段.routeTrack中定義的關(guān)系集合數(shù)量與routeTrackNum定義的關(guān)系集合數(shù)量有差異.即

式中：card(?)為笛卡爾積操作[7].

不變式表示系統(tǒng)的事件在執(zhí)行過程中應(yīng)遵守的屬性，需保證其在模型執(zhí)行的過程中始終為真.以精化模型1的機(jī)器文件為例，其中兩條安全屬性被表達(dá)成如下不變式：

1）任意兩條敵對(duì)進(jìn)路r1、r2不能同時(shí)被鎖閉，如式（8）.

式中：conflictRoute為敵對(duì)進(jìn)路集合.

2）一個(gè)軌道區(qū)段最多能被一條進(jìn)路鎖閉，如式（9）.

2.2 證明義務(wù)的證明

場景文件中的公理會(huì)產(chǎn)生證明義務(wù)，對(duì)其定義的合理性進(jìn)行檢查，機(jī)器文件中的不變式通過對(duì)相關(guān)事件生成證明義務(wù)的形式，實(shí)現(xiàn)對(duì)事件邏輯狀態(tài)的檢查.

以下是通過添加公理完善模型，使得證明義務(wù)得到證明通過的例子.

如對(duì)第4層模型中的rotate_switch_complete_2/inv1/INV證明義務(wù)進(jìn)行證明時(shí)，加入公理

式中：routeSwitchPos為建立進(jìn)路r中道岔sw應(yīng)被鎖閉的正確位置；dw為定位；fw為反位.

然后證明義務(wù)更新后未通過.分析過程如下：

在場景文件C4中，將routeSwitchPos定義為

式中：SWITCH為道岔的集合；道岔狀態(tài)SWITCH_POS={dw,fw,null}，null表示道岔處于四開狀態(tài).

可 見routeSwitchPos(r→ sw)的 值 可 能 是 null，故以上目標(biāo)不能得到證明.在C4文件中添加公理，如式（12）.

式中：r_otherSwitchPos為與routeSwitchPos關(guān)聯(lián)的雙動(dòng)道岔另一端的狀態(tài).

之后將式（12）添加作為該證明義務(wù)的假設(shè)，該證明義務(wù)得以成立.

本次建立的模型各層文件共計(jì)生成了710條證明義務(wù)，通過完善模型中的形式表達(dá)，結(jié)合手動(dòng)交互式證明策略，最后所有生成的證明義務(wù)都證明通過，統(tǒng)計(jì)情況如表2所示.

表2 模型證明義務(wù)的證明情況統(tǒng)計(jì)Tab.2 Proving statistics of model proof obligations 條

從需求文本到形式化模型的邏輯轉(zhuǎn)換跨度較大，且系統(tǒng)規(guī)范也可能存在漏洞.所以，證明義務(wù)的證明過程是完善系統(tǒng)的設(shè)計(jì)規(guī)范、修正系統(tǒng)屬性及形式化模型中潛在缺陷的重要手段[1].

3 數(shù)據(jù)確認(rèn)及功能仿真與測試

3.1 基于公理驗(yàn)證的數(shù)據(jù)確認(rèn)

以上各類證明義務(wù)全部通過，保證了聯(lián)鎖系統(tǒng)功能的可達(dá)性與安全性.若要保證實(shí)際車站聯(lián)鎖系統(tǒng)的可靠性還需要滿足：1）公理的正確性驗(yàn)證.證明義務(wù)的證明過程默認(rèn)公理的正確性，且將其作為證明條件；2）實(shí)際車站中聯(lián)鎖數(shù)據(jù)的安全性確認(rèn).聯(lián)鎖數(shù)據(jù)在人工編制過程中可能會(huì)發(fā)生錯(cuò)誤.

文中設(shè)計(jì)了如圖4所示的技術(shù)路線來進(jìn)行公理驗(yàn)證及數(shù)據(jù)確認(rèn)，即基于原模型1，建立一個(gè)僅有靜態(tài)場景文件的新模型2，將所有場景文件進(jìn)行實(shí)例化，即基于具體車站實(shí)例數(shù)據(jù)，對(duì)場景文件中的各常量進(jìn)行賦值，且將除數(shù)據(jù)定義外的各屬性公理設(shè)定為定理.該定理在系統(tǒng)中均可以自動(dòng)生成相應(yīng)的證明義務(wù)，通過證明來保證各公理的正確性.

圖4 數(shù)據(jù)確認(rèn)的技術(shù)方案Fig.4 Technical solution for data validation

本文實(shí)例選用的是圖5所示的典型三股道車站，編制了對(duì)應(yīng)的聯(lián)鎖表（只列出發(fā)車進(jìn)路6條操作，另有接車進(jìn)路6條未列出）如表3所示[9].

表3 舉例車站聯(lián)鎖表Tab.3 Interlocking table of the example station

圖5 舉例車站平面布置Fig.5 Layout of an example railway station

證明過程中，C1場景文件中定理routeTrackNum∈ROUTE→(TRACKZ ) 對(duì)應(yīng)的證明義務(wù)未被證明通過，其中ROUTE=1，2，···，12，TRACK={IG，IIG，IIIG，1/3DG，2/4DG}，routeTrackNum已被實(shí)例化為各條進(jìn)路中各軌道區(qū)段的連接序號(hào).分析得出原因?yàn)椋捍硕ɡ頌槎嗉?jí)函數(shù)關(guān)系，對(duì)應(yīng)狀態(tài)空間過大，超出了證明器的最大內(nèi)存容量占用限制.本文設(shè)計(jì)了一種等價(jià)狀態(tài)的證明方法如下：

1）定義 4 條公理：ROUTE1={1,2,3}，ROUTE2={4,5,6}，···，ROUTE4={10,11,12}，代替ROUTE=1,2,···,12，同時(shí)定義公理：

2）實(shí)例化routeTrackNum1，routeTrackNum2，···，routeTrackNum4 為進(jìn) 路ROUTE1，ROUTE2，···，ROUTE4對(duì)應(yīng)的區(qū)段，代替routeTrackNum的實(shí)例化數(shù)據(jù)，同時(shí)定義公理：

3）新定義 4 條定理

routeTrackNum1∈ROUTE1→(TRACKZ )，routeTrackNum2∈ROUTE2→(TRACKZ )，··，routeTrackNum4∈ROUTE4→(TRACKZ )，同時(shí)增加1條檢查定理，檢查routeTrackNum1，route-TrackNum2，···，routeTrackNum4 的定義域相互之間不出現(xiàn)重疊；

4）通過證明3）中5個(gè)較小狀態(tài)空間的定理，并將證明通過的定理做為原定理證明中的前提條件，從而實(shí)現(xiàn)了對(duì)原定理的證明.

上述內(nèi)容列在文件C1_1中，更改后驗(yàn)證結(jié)果如表4所示，可見在文件C1_1中，新增的5條定理和原定理共產(chǎn)生的6條證明義務(wù)全部可以證明通過.

表4 公理驗(yàn)證結(jié)果Tab.4 Verification of axioms 條

表4中的結(jié)果顯示，由上述車站編制的聯(lián)鎖數(shù)據(jù)達(dá)到了模型2中所有定理的要求，從而確認(rèn)了聯(lián)鎖數(shù)據(jù)，且證明了原模型中公理的正確性.在模型2中已證明所舉例車站聯(lián)鎖數(shù)據(jù)滿足原模型中所有公理約束.新建一個(gè)模型3，其場景文件從模型2擴(kuò)展而來，其機(jī)器文件由原模型中繼承而來.對(duì)模型3進(jìn)行死鎖及是否存在違反不變式的情況進(jìn)行檢驗(yàn)，結(jié)果顯示，模型無死鎖且不存在違反不變式的情況.

模型中的所有公理均是開發(fā)者根據(jù)對(duì)需求的分析后而形式化設(shè)定的，在分析的過程中可能會(huì)存在錯(cuò)誤的邏輯描述，或各公理之間可能存在矛盾.數(shù)據(jù)的可靠性是計(jì)算機(jī)聯(lián)鎖系統(tǒng)功能實(shí)現(xiàn)的基礎(chǔ).本文研究中通過基于公理驗(yàn)證的數(shù)據(jù)確認(rèn)方法，檢查并確認(rèn)了公理與數(shù)據(jù)的正確性.

3.2 驗(yàn)收測試與仿真實(shí)驗(yàn)

由于向不同領(lǐng)域的專家解釋形式化模型的屬性時(shí)存在困難，且非形式化研究人員很難確認(rèn)模型事件的正確性，因此通過驗(yàn)收測試與仿真實(shí)驗(yàn)的方式，以說明驗(yàn)證后的模型所能實(shí)現(xiàn)的功能.

Cucumber for Event-B[11]允許在 Event-B 模型中建立 Gherkin 場景（Gherkin scenarios），可以被用來編碼和執(zhí)行驗(yàn)收測試.根據(jù)所建立模型3，建立一個(gè)應(yīng)用Cucumber測試車站聯(lián)鎖進(jìn)路場景的例子，如圖6所示.其中：route_delay_L為列車進(jìn)路解鎖長延時(shí)事件，train_come_L為列車進(jìn)站事件，train_move_L為列車在進(jìn)路內(nèi)行駛事件，train_leave_L為列車離去事件，switch_delay_2為雙動(dòng)道岔轉(zhuǎn)動(dòng)計(jì)時(shí)事件；train、train_Pos、train_type分別為列車、列車位置、列車類型，e_t為進(jìn)站列車所接近的區(qū)段，L為列車類型集合.

圖6 測試場景的步驟定義Fig.6 Plain step definitions oftest scenario

基于驗(yàn)證后的模型3，使用BMotionWeb插件工具制作一個(gè)典型實(shí)際車站的執(zhí)行場景，可仿真不同變量與參數(shù)下的模型響應(yīng)結(jié)果，用以對(duì)聯(lián)鎖表的數(shù)據(jù)進(jìn)行功能確認(rèn).其中仿真場景中的燈色、道岔、列車的狀態(tài)直接與模型中的變量相關(guān)聯(lián).圖7中為演示聯(lián)鎖表中第10條即股道Ⅰ至發(fā)車進(jìn)路S建立的場景，其中發(fā)車信號(hào)機(jī)XI顯示為綠色燈光，在仿真執(zhí)行過程中，車輛、色燈、道岔、進(jìn)路與區(qū)段的狀態(tài)變化都與設(shè)計(jì)規(guī)范相符.

圖7 仿真測試舉例Fig.7 Example of simulation testing

按照?qǐng)D5中車站對(duì)應(yīng)的聯(lián)鎖表，在驗(yàn)收測試與可視化仿真環(huán)境中逐條建立和解鎖進(jìn)路，系統(tǒng)功能均可正常實(shí)現(xiàn).上述過程對(duì)形式化模型進(jìn)行了功能化的描述，同時(shí)還對(duì)模型的正確性做出檢查，即通過仿真實(shí)驗(yàn)和驗(yàn)收測試，可以檢測用戶場景的集合，為系統(tǒng)行為的可達(dá)性提供了明確的說明，可進(jìn)一步檢查模型功能是否正確，與系統(tǒng)設(shè)計(jì)規(guī)范是否一致.

4 結(jié) 論

本文建立了基于規(guī)范分析得出通用系統(tǒng)形式化描述的過程，提出了一種對(duì)系統(tǒng)行為進(jìn)行驗(yàn)證的方法.基于規(guī)范分析得出系統(tǒng)設(shè)計(jì)的環(huán)境屬性、功能屬性、安全屬性與各事件流程，輔助使用UML工具建立初始模型的場景文件與機(jī)器文件，描述了各屬性與事件流程；對(duì)本層的證明義務(wù)進(jìn)行定理證明，基于精化策略，建立了后續(xù)各層模型.通過驗(yàn)證各層模型的系統(tǒng)屬性，完善了通用功能模型.基于一個(gè)實(shí)例車站的聯(lián)鎖數(shù)據(jù)對(duì)系統(tǒng)中公理的正確性進(jìn)行驗(yàn)證，并通過檢驗(yàn)是否存在死鎖與違反不變式的情況，進(jìn)一步確認(rèn)了模型的可靠性.

文中提出了基于通用形式化模型對(duì)系統(tǒng)數(shù)據(jù)進(jìn)行確認(rèn)的方法，即將聯(lián)鎖數(shù)據(jù)注入驗(yàn)證后的模型中，可以有效地進(jìn)行聯(lián)鎖數(shù)據(jù)的驗(yàn)證；并通過功能仿真與驗(yàn)收測試技術(shù)，直觀地展現(xiàn)模型的功能特性，可進(jìn)一步驗(yàn)證系統(tǒng)行為，并同時(shí)對(duì)聯(lián)鎖數(shù)據(jù)的正確性進(jìn)行了檢驗(yàn).

備注：本文相關(guān)的模型文件可在文獻(xiàn)[10]的鏈接中下載.