形式化自動測試在計算機聯(lián)鎖系統(tǒng)中的應(yīng)用研究

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

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

1 形式化自動測試概述

1.1 形式化方法

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

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

1.2 形式化自動測試基礎(chǔ)

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

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

表1 PiSPEC語言常用謂詞邏輯表達

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

Test Case:用例名稱

Foreach（對象變量名）｛

賦值語句；

Expect語句；｝

2 形式化自動測試方案

2.1 整體方案

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

圖1 自動測試方案流程圖

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

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

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

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

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

2.2 形式化建模

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

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

3 測試用例設(shè)計

3.1 測試說明

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

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

3.2 測試用例描述

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

表2 JBLS-0006測試用例自然語言描述

3.3 測試用例分解

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

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

圖2 測試用例JBLS-0006的測試流程

3.4 形式化測試腳本

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

圖3 JBLS-0006用例主體代碼

4 仿真測試

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

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

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

圖4 SII-X實例化用例代碼

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

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

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

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

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

［action］模擬進路始端信號重新開放（-LRC=1）

［expect］進路始端信號重開（-LXJ=1）

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

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

圖5 變量的梯形圖

5 結(jié)論

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

1）形式化自動測試速度快,可以大大減少測試時間和人力的投入。

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

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

4）當需求或測試用例升級時,形式化測試代碼修改方便。

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

形式化自動測試的優(yōu)勢顯著,未來在自動化測試領(lǐng)域?qū)⒕哂泻軓姷母偁幜Α?/p>