張銘瑤，王燕芩，李衛(wèi)娟，楊平

計(jì)算機(jī)聯(lián)鎖系統(tǒng)是鐵路信號(hào)領(lǐng)域的安全關(guān)鍵系統(tǒng),對(duì)該系統(tǒng)的功能與安全測(cè)試尤為重要?，F(xiàn)有自動(dòng)測(cè)試的研究多針對(duì)黑盒測(cè)試,更加注重測(cè)試結(jié)果。而基于形式化方法的自動(dòng)測(cè)試可應(yīng)用于白盒測(cè)試,方便系統(tǒng)參數(shù)的追蹤,透明化測(cè)試執(zhí)行過程,提高測(cè)試結(jié)果可信度。本文重點(diǎn)研究形式化自動(dòng)測(cè)試在聯(lián)鎖系統(tǒng)中的應(yīng)用,并展示測(cè)試用例的執(zhí)行結(jié)果。

1 形式化自動(dòng)測(cè)試概述

1.1 形式化方法

形式化方法以數(shù)學(xué)為基礎(chǔ),利用數(shù)學(xué)的嚴(yán)謹(jǐn)性和精確性來描述和設(shè)計(jì)系統(tǒng),具有較好的可讀性、準(zhǔn)確性、無二義性等語言特點(diǎn)［1］。在軌道交通領(lǐng)域,形式化方法的研究和應(yīng)用越來越熱門:有研究適用于計(jì)算機(jī)處理的鐵路信號(hào)領(lǐng)域形式化表達(dá)方法,以替代傳統(tǒng)繼電器接點(diǎn)電路的邏輯關(guān)系處理方式［4］；有采用基于梯形圖邏輯的形式化驗(yàn)證方法,實(shí)現(xiàn)基于NuSMV的鐵路聯(lián)鎖系統(tǒng)設(shè)計(jì)模型的形式化驗(yàn)證［5］；有建立計(jì)算機(jī)聯(lián)鎖軟件道岔定位需求模型,并在CBTC聯(lián)鎖系統(tǒng)軟件設(shè)計(jì)中予以應(yīng)用［6］；有采用時(shí)間自動(dòng)機(jī)的形式化建模和驗(yàn)證方法,驗(yàn)證自主化ATP系統(tǒng)是否滿足期望的系統(tǒng)性質(zhì)［7］；有以鐵路運(yùn)營(yíng)場(chǎng)景為核心,實(shí)現(xiàn)基于SED_TSL的高速鐵路列控中心系統(tǒng)自動(dòng)化測(cè)試環(huán)境的搭建［8］；有研究基于模型的形式化測(cè)試案例和測(cè)試序列生成方法,并應(yīng)用于ETCS-2級(jí)系統(tǒng)測(cè)試［9］。

目前,形式化方法的研究主要分為3個(gè)方面:形式化建模、形式化驗(yàn)證和形式化自動(dòng)測(cè)試。其中,建模是驗(yàn)證和測(cè)試的基礎(chǔ)。本文重點(diǎn)研究形式化測(cè)試在計(jì)算機(jī)聯(lián)鎖系統(tǒng)中的應(yīng)用,用以輔助形式化驗(yàn)證,完成系統(tǒng)安全功能的測(cè)試。

1.2 形式化自動(dòng)測(cè)試基礎(chǔ)

形式化自動(dòng)測(cè)試的基礎(chǔ)是自動(dòng)化測(cè)試工具和形式化腳本語言。本文研究的形式化自動(dòng)測(cè)試采用瑞典Prover Technology AB公司提供的Prover iLock工具套件,集形式化開發(fā)、形式化驗(yàn)證、形式化測(cè)試為一體,提供圖形化界面,為驗(yàn)證和測(cè)試提供直觀的調(diào)試功能,并支持特定應(yīng)用數(shù)據(jù)的配置,使測(cè)試平臺(tái)具有通用性,支持PiSPEC形式語言。

形式化自動(dòng)測(cè)試中通用測(cè)試用例（Generic Test Specification,GTS）,形 式 化 腳 本 采 用PiSPEC語言描述。PiSPEC語言是一種基于形式化語法的邏輯描述語言,使用謂詞邏輯進(jìn)行安全需求和測(cè)試用例的形式化描述。該語言的規(guī)約包括輸入變量Inputs、輸出變量Outputs、中間變量Equations、時(shí)間變量Timers、函數(shù)Functions、參數(shù)Parameters、賦值語句Procedure、測(cè)試用例TestCase等。PiSPEC語言的基礎(chǔ)是謂詞邏輯,表1列出了GTS中常用謂詞邏輯。

表1 PiSPEC語言常用謂詞邏輯表達(dá)

大部分測(cè)試用例需要遍歷站場(chǎng)對(duì)象,因此在測(cè)試用例腳本中使用率較高的是Foreach遍歷語句,遍歷語句一般和期望語句Expect結(jié)合,用于判斷用戶對(duì)象是否滿足測(cè)試用例場(chǎng)景。實(shí)例化后,若Expect判定結(jié)果為真,則用戶對(duì)象滿足定義的用例場(chǎng)景,判定為測(cè)試通過；否則測(cè)試失敗?；赑iSPEC的形式化測(cè)試用例語言結(jié)構(gòu)為

Test Case:用例名稱

Foreach（對(duì)象變量名）｛

賦值語句；

Expect語句；｝

2 形式化自動(dòng)測(cè)試方案

2.1 整體方案

自動(dòng)測(cè)試將測(cè)試用例和聯(lián)鎖數(shù)據(jù)作為輸入,Prover iLock讀取輸入并根據(jù)聯(lián)鎖邏輯自行進(jìn)行中間運(yùn)算,最后對(duì)目標(biāo)狀態(tài)進(jìn)行判定。目標(biāo)狀態(tài)滿足期望則認(rèn)為測(cè)試通過,否則不通過。自動(dòng)測(cè)試方案的流程見圖1,它包括5個(gè)子流程。

圖1 自動(dòng)測(cè)試方案流程圖

1）自然語言描述的系統(tǒng)模型和測(cè)試用例說明書:系統(tǒng)模型是對(duì)聯(lián)鎖系統(tǒng)站場(chǎng)設(shè)備構(gòu)建的屬性模型,自然語言描述的系統(tǒng)模型即對(duì)象模型,以表格形式構(gòu)建。對(duì)每一個(gè)站場(chǎng)設(shè)備對(duì)象建立一個(gè)表格類以描述其屬性,包括聯(lián)鎖輸入/輸出/中間變量、對(duì)象關(guān)系、繼承關(guān)系、函數(shù)等。

2）系統(tǒng)模型和測(cè)試用例進(jìn)行形式化轉(zhuǎn)換:將步驟1中的系統(tǒng)模型和測(cè)試用例采用PiSPEC形式化語言描述。

3）特定站場(chǎng)數(shù)據(jù)轉(zhuǎn)化:通過翻譯器將聯(lián)鎖輸入數(shù)據(jù)轉(zhuǎn)換為iLOCK可識(shí)別的LCF格式文件,輸入數(shù)據(jù)包括TLE站場(chǎng)數(shù)據(jù)、聯(lián)鎖布爾文件、車站信息聯(lián)鎖表、聯(lián)鎖與軌旁設(shè)備接口信息表、聯(lián)鎖與其他子系統(tǒng)接口信息表等。

4）iLOCK工具進(jìn)行實(shí)例化編譯:Prover iLock工具提供實(shí)例化按鈕,該步執(zhí)行完畢后可以在可視化界面上查看完整站場(chǎng)圖及站場(chǎng)對(duì)象的屬性,且站場(chǎng)圖層的設(shè)備對(duì)象與底層代碼級(jí)的對(duì)象模型成功建立聯(lián)系。

5）仿真器中執(zhí)行測(cè)試用例進(jìn)行仿真調(diào)試:仿真器是Prover iLock工具提供的執(zhí)行測(cè)試用例的組件,提供調(diào)試界面,便于模擬測(cè)試場(chǎng)景和跟蹤測(cè)試用例執(zhí)行結(jié)果；對(duì)于運(yùn)行失敗的測(cè)試用例可以進(jìn)一步調(diào)試來查找失敗原因；提供文件生成功能,對(duì)測(cè)試結(jié)果自動(dòng)生成測(cè)試報(bào)告。

2.2 形式化建模

形式化測(cè)試方案中,構(gòu)建形式化對(duì)象模型是基礎(chǔ),對(duì)象模型用于定義鐵路站場(chǎng)設(shè)備對(duì)象及屬性。構(gòu)建對(duì)象模型時(shí),將有共同屬性的一類設(shè)備抽象成一個(gè)對(duì)象類,對(duì)象類的屬性包括:輸入變量Inputs、輸 出 變 量Outputs、中 間 變 量Equations、時(shí)間變量Timers、函數(shù)Functions、參數(shù)Parameters等。

自動(dòng)測(cè)試涉及的主要站場(chǎng)對(duì)象類型包括:信號(hào)機(jī)、道岔、軌道區(qū)段、進(jìn)路等,每種類型又可以衍生出不同的子類型,如信號(hào)機(jī)可分為出站信號(hào)機(jī)、進(jìn)站信號(hào)機(jī)、出站兼調(diào)車信號(hào)機(jī)、進(jìn)路信號(hào)機(jī)、調(diào)車信號(hào)機(jī)等子類型,父類和子類之間存在繼承關(guān)系。代碼層對(duì)象模型建立后,通過配置文件將站場(chǎng)設(shè)備對(duì)象與PiSPEC構(gòu)建的對(duì)象類建立映射連接,保證實(shí)例化后對(duì)象模型與站場(chǎng)設(shè)備相對(duì)應(yīng)。

3 測(cè)試用例設(shè)計(jì)

3.1 測(cè)試說明

選用站型較復(fù)雜的標(biāo)準(zhǔn)站作為測(cè)試站,站場(chǎng)規(guī)模:信號(hào)機(jī)140個(gè)、道岔45組、區(qū)段127個(gè)、列車進(jìn)路214條、調(diào)車進(jìn)路240條。目前設(shè)計(jì)的測(cè)試用例包括2條道岔相關(guān)用例和24條進(jìn)路相關(guān)用例。道岔相關(guān)的用例測(cè)試道岔定位/反位操作及表示；進(jìn)路相關(guān)的用例主要測(cè)試進(jìn)路上道岔、信號(hào)機(jī)、軌道電路間的基本聯(lián)鎖關(guān)系。在仿真器中執(zhí)行每條用例對(duì)測(cè)試對(duì)象的覆蓋率均可達(dá)100%,26條用例在仿真器中平均運(yùn)行時(shí)間約15 min。

以一條進(jìn)路用例JBLS-0006為例,闡述測(cè)試用例設(shè)計(jì)過程。

3.2 測(cè)試用例描述

根據(jù)《鐵路計(jì)算機(jī)聯(lián)鎖技術(shù)條件》,對(duì)于已經(jīng)開放的信號(hào)機(jī),當(dāng)進(jìn)路上軌道電路條件不滿足時(shí)信號(hào)應(yīng)及時(shí)關(guān)閉［10］,測(cè)試用例JBLS-0006的詳細(xì)描述見表2。

表2 JBLS-0006測(cè)試用例自然語言描述

3.3 測(cè)試用例分解

從測(cè)試用例JBLS-0006中提取對(duì)象模型,對(duì)象模型中,ROUTE類包含了2個(gè)關(guān)系:①start_signal（rt,si）表示信號(hào)機(jī)si是進(jìn)路rt的始端信號(hào)；②inside_tracks（rt,tc）表示區(qū)段tc是進(jìn)路rt內(nèi)方區(qū)段。列車進(jìn)路類和調(diào)車進(jìn)路類是進(jìn)路類的2個(gè)子類,列車父信號(hào)和調(diào)車父信號(hào)是信號(hào)類的2個(gè)子類。

該條測(cè)試用例是對(duì)鎖閉進(jìn)路內(nèi)的軌道區(qū)段進(jìn)行遍歷,模擬區(qū)段占用,預(yù)期結(jié)果為進(jìn)路始端信號(hào)關(guān)閉。以列車進(jìn)路為例,用例流程見圖2。

圖2 測(cè)試用例JBLS-0006的測(cè)試流程

3.4 形式化測(cè)試腳本

將上述流程圖轉(zhuǎn)化為以PiSPEC語言描述的JBLS-0006測(cè)試用例的主體代碼,見圖3。測(cè)試步驟中采用Foreach（list）語句遍歷站場(chǎng)設(shè)備對(duì)象,預(yù)期結(jié)果采用Expect語句。當(dāng)測(cè)試結(jié)果滿足預(yù)期結(jié)果時(shí)則測(cè)試通過,否則不通過。代碼的可讀性較強(qiáng),具有面向?qū)ο笳Z言的可封裝性和繼承性等特點(diǎn)。其中,ClearDetected對(duì)應(yīng)聯(lián)鎖系統(tǒng)中的區(qū)段占用/出清狀態(tài)DGJ-DI；TrainOpen對(duì)應(yīng)聯(lián)鎖系統(tǒng)中信號(hào)開放/關(guān)閉的變量LXJ。

圖3 JBLS-0006用例主體代碼

4 仿真測(cè)試

以鐵路標(biāo)準(zhǔn)站作為測(cè)試站,在仿真器中運(yùn)行測(cè)試用例,用例遍歷全部道岔共86個(gè)（45組）,全部進(jìn)路共454條,測(cè)試覆蓋率達(dá)100%。當(dāng)前26條測(cè)試用例共執(zhí)行Expect判斷項(xiàng)11 045條,通過10 069條,失敗976條,執(zhí)行時(shí)間15 min 28 s。仿真界面上可通過用例顏色區(qū)分測(cè)試結(jié)果,綠色用例為通過,紅色用例表示執(zhí)行失敗。

對(duì)于每條測(cè)試用例結(jié)果可進(jìn)一步跟蹤測(cè)試過程,如要查看JBLS-0006用例中SII-X列車進(jìn)路的執(zhí)行情況:可在調(diào)試窗中的Results標(biāo)簽查看每一步期望的結(jié)果是否通過；在Test case標(biāo)簽中查看用例實(shí)例化代碼,并可根據(jù)結(jié)果逐步調(diào)試；通過Schema標(biāo)簽查看聯(lián)鎖變量的梯形邏輯圖。借助上述輔助功能,形式化自動(dòng)測(cè)試可起到白盒測(cè)試的作用,不僅能看到測(cè)試結(jié)果,還可查看中間過程,當(dāng)測(cè)試用例不通過時(shí),可以借助這些輔助功能快速定位用例失敗原因。

圖4 為進(jìn)路SII-X的JBLS-0006用例在仿真系統(tǒng)中自動(dòng)實(shí)例化后生成的代碼,該進(jìn)路區(qū)段包括51DG,27-33DG,29-31DG,11-23DG,1-7DG,IAG。根據(jù)表2的測(cè)試步驟將實(shí)例化代碼拆分成以下4個(gè)部分,其中每一步列出了實(shí)例化對(duì)應(yīng)的主要聯(lián)鎖變量,［action］主要執(zhí)行對(duì)輸入變量的賦值,［expect］是對(duì)輸出或中間變量的值進(jìn)行判定。

圖4 SII-X實(shí)例化用例代碼

步驟①:［action］輸入始終端命令（-LRC=1,-LXS=1）

［expect］進(jìn)路顯示白光帶（-W=1）,進(jìn)路始端信號(hào)在4s內(nèi)開放（-LXJ=1）

步驟②:［action］模擬進(jìn)路上區(qū)段占用（-DGJ-DI=0）

［expect］進(jìn)路始端信號(hào)關(guān)閉（-LXJ=0）

步驟③:［action］模擬進(jìn)路上區(qū)段出清（-DGJ-DI=1）

［action］模擬進(jìn)路始端信號(hào)重新開放（-LRC=1）

［expect］進(jìn)路始端信號(hào)重開（-LXJ=1）

步驟④:重復(fù)步驟③,遍歷進(jìn)路上全部區(qū)段。

梯形邏輯見圖5,用來呈現(xiàn)聯(lián)鎖布爾的實(shí)現(xiàn)邏輯及對(duì)應(yīng)繼電器接點(diǎn)的連通情況,并可查看執(zhí)行周期內(nèi)各聯(lián)鎖變量的實(shí)時(shí)狀態(tài)值。

圖5 變量的梯形圖

5 結(jié)論

本文采用基于對(duì)象模型的形式化自動(dòng)測(cè)試方法,使用形式化高級(jí)語言PiSPEC編寫測(cè)試用例,并給出了測(cè)試用例在Prover iLock仿真器的執(zhí)行結(jié)果,測(cè)試結(jié)果可追溯,每個(gè)周期系統(tǒng)內(nèi)邏輯變量的值可跟蹤。對(duì)比傳統(tǒng)的測(cè)試方法,形式化自動(dòng)測(cè)試具有以下優(yōu)點(diǎn)。

1）形式化自動(dòng)測(cè)試速度快,可以大大減少測(cè)試時(shí)間和人力的投入。

2）凡測(cè)試用例代碼覆蓋到的測(cè)試項(xiàng)均可執(zhí)行,避免人為失誤導(dǎo)致遺漏測(cè)試項(xiàng)。

3）測(cè)試用例代碼可復(fù)用,對(duì)不同的測(cè)試站只需要改變輸入的聯(lián)鎖數(shù)據(jù)即可。

4）當(dāng)需求或測(cè)試用例升級(jí)時(shí),形式化測(cè)試代碼修改方便。

5）生成的測(cè)試結(jié)果方便開展參數(shù)狀態(tài)分析和追蹤,測(cè)試過程透明化,增加自動(dòng)測(cè)試結(jié)果的可信任度。

形式化自動(dòng)測(cè)試的優(yōu)勢(shì)顯著,未來在自動(dòng)化測(cè)試領(lǐng)域?qū)⒕哂泻軓?qiáng)的競(jìng)爭(zhēng)力。