基于標簽轉(zhuǎn)移系統(tǒng)的二乘二取二系統(tǒng)的形式化驗證研究

付 偉

(中國鐵道科學研究院通信信號研究所,北京 100081)

1 概述

隨著鐵路列車控制技術的快速發(fā)展，具有我國自主產(chǎn)權的CTCS列車控制系統(tǒng)在我國高速鐵路上得到了廣泛應用，有效保障了高速列車的安全運行[1]。CTCS系統(tǒng)中的計算機聯(lián)鎖、列控、無線閉塞以及臨時限速等多個安全苛求系統(tǒng)大都采用二乘二取二架構形式[2-3]。

為了保證安全苛求系統(tǒng)安全可靠的運轉(zhuǎn)，對系統(tǒng)性能的分析和驗證顯得尤為重要。與傳統(tǒng)的測試手段不同，形式化方法具有的數(shù)學基礎，為系統(tǒng)的模型設計和驗證提供了嚴格驗證手段，形式化方法是一種新型嚴格意義上的驗證方法，被IEC50128等國際標準或者行業(yè)規(guī)范推薦使用。形式化方法在列車控制安全苛求系統(tǒng)中得到了廣泛的應用[4-9]。

安全苛求系統(tǒng)的模式轉(zhuǎn)換存在復雜性，標簽轉(zhuǎn)移系統(tǒng)(LTS)在處理系統(tǒng)復雜行為中具有良好的驗證功能，并在安全通信協(xié)議RSSP-1協(xié)議[10]，ERTMS/ETCS需求[11]分析與實現(xiàn)中得到了應用。針對二乘二取二安全苛求系統(tǒng)，使用標簽轉(zhuǎn)移系統(tǒng)進行建模分析，驗證了系統(tǒng)的安全使用性。

2 二乘二取二的安全苛求系統(tǒng)

2.1 二乘二取二安全苛求系統(tǒng)架構

二乘二取二系統(tǒng)由兩個功能完全相同的系統(tǒng)A系和B系組成，每個系統(tǒng)是二取二結(jié)構，A系和B系兩個系統(tǒng)構成雙機熱備冗余模式。兩個系統(tǒng)通過硬件配置區(qū)分A系或者B系。正常工作時，一系為主控，控制整個系統(tǒng)的輸出；另一系為備用，隨時準備替換出現(xiàn)問題的主控系統(tǒng)。為了實現(xiàn)人為選擇控制功能，系統(tǒng)中配置了切換控制手柄，手柄有3個狀態(tài)：A系主控、B系主控或者自動模式。不需要人工干預時手柄指向自動位置。人工也可以通過旋轉(zhuǎn)手柄，強制將A系或者B系升級為主控狀態(tài)

任意一個系統(tǒng)A系或者B系，包括兩個CPU(一個主CPU，一個從CPU)用以實現(xiàn)二取二比較；兩塊CAN通信板，與外部采集驅(qū)動板FIMO和FIMI系統(tǒng)進行采集驅(qū)動信息交互；若干外部以太網(wǎng)通信板，用以和其他安全苛求系統(tǒng)實現(xiàn)安全控制信息，系統(tǒng)實時狀態(tài)等關鍵信息交互；為了減少系統(tǒng)的共模錯誤，比較板作為第三方硬件比較器，實現(xiàn)主從CPU板上總線數(shù)據(jù)的實時校核[6]。整個安全苛求系統(tǒng)結(jié)構如圖1所示。

圖1 二乘二取二系統(tǒng)構成

2.2 二乘二取二系統(tǒng)工作模式

二乘二取二系統(tǒng)的工作方式采用雙系互為主、備，能實現(xiàn)“無擾”自動切換，且人工手動切換優(yōu)先的主備冗余方式[12-14]。

系統(tǒng)有主控、備用、初始化、聯(lián)機和離線5種穩(wěn)定狀態(tài)[15]。

主控狀態(tài)是指計算機系統(tǒng)具有控制權的工作狀態(tài)，此種狀態(tài)只有在確認另一系不是主控狀態(tài)且本系擁有控制權時才能發(fā)生。具備主控狀態(tài)的系統(tǒng)稱為主系。

備用狀態(tài)是指計算機系統(tǒng)通過同步相關數(shù)據(jù)，已使本身數(shù)據(jù)狀態(tài)與主系的對應狀態(tài)一致，并保持一致的輸出。具備主控狀態(tài)的系統(tǒng)稱為備系。備系應具備隨時以“無擾”切換方式接替主機工作的能力，切換與狀態(tài)的轉(zhuǎn)換必須嚴格遵循安全、可靠、合理的切換原則，一般以主系“離線”為先決條件。

初始化狀態(tài)是指計算機系統(tǒng)從關機到上電啟動，或從其他狀態(tài)復位重啟時初始階段的工作狀態(tài)。通常只有人工操作或意外斷電等某些導致復位啟動的故障，可使計算機系統(tǒng)進入初始化狀態(tài)。

聯(lián)機狀態(tài)是指本系與另一處于主控狀態(tài)的系統(tǒng)建立同步傳輸鏈接，將關鍵狀態(tài)數(shù)據(jù)交互，復制同步環(huán)境的工作狀態(tài)。

離線狀態(tài)也稱脫機狀態(tài)，是指計算機系統(tǒng)已退出上述4種正常工作狀態(tài)以外的其他狀態(tài)。通常計算機系統(tǒng)因發(fā)現(xiàn)故障、失步而自動退出，手柄切換強制退出正常所在狀態(tài)都導致其進入離線狀態(tài)；運行中關機、掉電、程序死鎖等原因?qū)е碌乃罊C狀態(tài)也屬于離線狀態(tài)。

上述5種狀態(tài)中，主控狀態(tài)、同步狀態(tài)和離線狀態(tài)是長期穩(wěn)定工作狀態(tài)。聯(lián)機狀態(tài)為短暫過渡狀態(tài)；初始化狀態(tài)由于其系統(tǒng)狀態(tài)標志在建立中，可以認為是離線狀態(tài)的一種特殊形式。

A系和B系的兩系統(tǒng)所有5種狀態(tài)的組合關系如表1所示。由表1可以看出，25種狀態(tài)組合中，只有12種情況是允許出現(xiàn)的。

表1 二乘二取二系統(tǒng)轉(zhuǎn)換關系

2.3 系統(tǒng)工作模式轉(zhuǎn)換處理機制

系統(tǒng)程序根據(jù)切換手柄的狀態(tài)、系統(tǒng)各自的工作狀態(tài)并配合檢查對方系的工作狀態(tài)來處理和實現(xiàn)工作模式的無縫轉(zhuǎn)換。系統(tǒng)工作模式切換機制如圖2所示。

圖2 系統(tǒng)工作模式轉(zhuǎn)換流程

當手柄處于自動位置，系統(tǒng)設置為自動模式。系統(tǒng)啟動上電后進入初始化狀態(tài)。初始化狀態(tài)進行系統(tǒng)狀態(tài)檢查，具體包括本系和另系狀態(tài)繼電器接點閉合情況。如果初始化檢查不通過不能進入主控狀態(tài)。如果上電時手柄在手動位置，則手柄指向的一系在初始化檢查正常后進入主控狀態(tài)，另一系不需要對狀態(tài)繼電器進行檢查，維持離線狀態(tài)。

系統(tǒng)程序正常工作后，需要進行周期檢查，即每個運行周期要檢測手柄和兩系的狀態(tài)繼電器的狀態(tài)和系統(tǒng)關鍵變量狀態(tài)，以此決定本系下一周期的工作狀態(tài)。其中，檢查關鍵變量包括嚴重錯誤標志、主從CPU板的輸出比較結(jié)果、兩系間的輸入輸出比較結(jié)果、兩系間的通信狀態(tài)、通過ETH板卡連接的其他安全苛求系統(tǒng)的通信狀態(tài)等因素。系統(tǒng)在周期檢查失敗后將進入離線狀態(tài)。

系統(tǒng)正常運行時，一系主控，另一系備用。除了在初始化階段系統(tǒng)通過檢查后可以直接升為主控狀態(tài)的情況，在正常運行中，系統(tǒng)只能從備用狀態(tài)進入主控，且前提是確認原主系已離線。另外，系統(tǒng)只能從離線狀態(tài)進入聯(lián)機狀態(tài)，只能從聯(lián)機狀態(tài)進入備用狀態(tài)。

聯(lián)機狀態(tài)為過渡狀態(tài)。本系向成為主控狀態(tài)的另一系聯(lián)機時，首先向主系發(fā)送申請，在收到主系回復的同步狀態(tài)信息后，用其初始化本系程序的變量數(shù)據(jù)，當本系的輸出與主系比較結(jié)果一致時兩系同步，本系變?yōu)閭溆脿顟B(tài)。如果未能收到回復的狀態(tài)同步信息或者與主系輸出不一致，則本系離線，延遲一段時間后重新進行聯(lián)機操作。

3 系統(tǒng)邏輯的模型驗證

3.1 轉(zhuǎn)移標簽系統(tǒng)(LTS)

LTS轉(zhuǎn)移標簽系統(tǒng)由一系列過程P組成，P可以用四元素，描述，其中

(1)Q是由非空狀態(tài)集合；

(2)A=α(P)∪{τ}是有限的標簽集，其中α(P)表示字母表P，τ為包括內(nèi)部行為，不為外部環(huán)境所知；

(3)Λ?Q×A×Q代表一個轉(zhuǎn)移關系；

(4)q0∈Q，是Q的初始狀態(tài)。

LTSA軟件是一個系統(tǒng)行為分析驗證工具，模擬系統(tǒng)交互行為，檢查系統(tǒng)并發(fā)行為是否滿足系統(tǒng)需求。LTSA軟件將系統(tǒng)行為描述成一系列交互狀態(tài)機。每一個需求被描述成一個LTS組件，包括組件可能達到的所有狀態(tài)和轉(zhuǎn)移情況。LTSA軟件通過組件可達性分析，遍歷搜索組件的錯誤行為。LTSA軟件支持過程代數(shù)定義，如有限狀態(tài)過程FSP語言的組件行為描述，可以將相應的FSP需求組件行為圖形化顯示。

3.2 系統(tǒng)模式轉(zhuǎn)換建模

根據(jù)圖2的平臺邏輯處理，對于一系的字母集定義如下

A={inichk，inisysOK，inisysBad，cycchk，cycsysOK，cycsysBad，reInit，othOffline，othMainControl，checksw，checkOth，standBy，swtoself，swtoOth，swtoAuto，swAuto，swSelf，swOth}

動作列表如表2所示，系統(tǒng)交互行為使用FSP語言建模如下

S=S1，

S1=(inichk->inisysOK->checksw->swAuto->checkOth->othOffline->S2

|inichk->inisysOK->checksw->swSelf->S2

|inichk->inisysOK->checksw->swOth->S3

|inichk->inisysOK->checksw->swAuto->checkOth->othMainControl->S4

|inichk->inisysBad->S1)，

S2=(inichk->inisysBad->checksw->swAuto->S3

|reInit->S1)，

S3=(swtoself->checkOth->othOffline->S2

|checksw->swAuto->cycchk->cycsysOK->S4

|checksw->swOth->S3)，

S4=(checksw->swAuto->checkOth->othMainControl->standBy->S5

|checksw->swAuto->cycchk->cycsysBad->S3

|swtoOth->swOth->S3

|reInit->S1)，

S5=(checksw->swAuto->cycchk->cycsysBad->S3

|swtoOth->S3

|checksw->swAuto->checkOth->othOffline->S2

|swtoSelf->swSelf->checkOth->othOffline->S2).

借助LTSA軟件，系統(tǒng)模式轉(zhuǎn)換的LTS模型轉(zhuǎn)換狀態(tài)如圖3所示。圖3表明系統(tǒng)模式轉(zhuǎn)換邏輯的狀態(tài)存在47個臨時狀態(tài)，交互過程中不存在死鎖現(xiàn)象。

圖3 系統(tǒng)模式轉(zhuǎn)換LTS模型

操作描述操作描述inichk本系初始化檢查checksw檢查手柄狀態(tài)inisysOK本系初始檢查正常checkOth本系檢查另一系的狀態(tài)inisysBad本系初始檢查失敗standBy本系聯(lián)機另一系cycchk本系周期檢查swtoself手柄轉(zhuǎn)向本系cycsysOK本系周期檢查正常swtoOth手柄轉(zhuǎn)向另一系cycsysBad本系周期檢查失敗swtoAuto手柄轉(zhuǎn)向自動位置reInit本系重新初始化swAuto手柄處于自動位置othOffline另一系處于離線狀態(tài)swSelf手柄處于指向本系的位置othMainControl另一系處于主控狀態(tài)swOth手柄處于指向另系的位置

4 安全性分析

在系統(tǒng)模式轉(zhuǎn)換邏輯中，如果某些錯誤發(fā)生，應該按照故障-安全原則，狀態(tài)需要導向安全側(cè)。如下系統(tǒng)行為在模式轉(zhuǎn)換過程中不允許發(fā)生。

(1)本系初始化檢查錯誤本系不能聯(lián)機另一系。

(2)本系周期巡檢錯誤，不能聯(lián)機另一系。

通過LTSA軟件的安全屬性進行檢驗。威脅行為的安全屬性由FSP語言建模如下

propertySafety=Safe，

Safe=(inisysBad->standBy->Safe

|cycsysBad->standBy->Safe).

使用LTSA軟件驗證屬性結(jié)果如圖4所示。圖4中狀態(tài)標簽‘-1’代表錯誤狀態(tài)。系統(tǒng)安全屬性(1)和系統(tǒng)安全屬性(2)都滿足安全原則。

圖4 平臺模式轉(zhuǎn)換安全屬性LTA模型

5 形式化驗證應用和性能分析

LTS形式化方式應用在二乘二取二系統(tǒng)，克服了異常錯誤，概念歧義等問題。為了便于對比，安全苛求平臺分別使用上述推薦方法和傳統(tǒng)人工驗證方法進行開發(fā)測試，最后軟件通過C語言實現(xiàn)并在DOS操作系統(tǒng)實現(xiàn)。

兩個開發(fā)小組獨立使用LTS方法和人工驗證方法的記錄如表3所示。記錄項包括兩種方法設計的程序缺陷數(shù)目，系統(tǒng)完成費時量。從表3可以看出，采用LTS模型方法產(chǎn)生的程序缺陷數(shù)目比傳統(tǒng)人工方法少64%。同時，系統(tǒng)開發(fā)工作量節(jié)省29%。結(jié)果表明，LTS方法為系統(tǒng)開發(fā)者縮短了設計實現(xiàn)周期并提高了開發(fā)質(zhì)量。

表3 驗證方法結(jié)果對比

6 結(jié)語

本文介紹了一種基于LTS模型驗證方法，并在二乘二取二平臺的實際開發(fā)工程應用。根據(jù)平臺的交互行為和安全屬性建立的LTS模型，通過LTSA軟件進行了驗證，驗證結(jié)果對于實時安全苛求系統(tǒng)的設計者和開發(fā)者具有極大的幫助。

[1] 郭玉華.借鑒ETCS完善CTCS技術規(guī)范體系的研究[J].鐵道標準設計，2016，60(10)：136-140.

[2] WANG X， Ma L C H， Tang T. Study on formal modeling and verification of safety computer platform[J]. Advances in Mechanical Engineering， 2016，8(5)：1-13.

[3] 季忠紅，王俊高，馮浩楠.基于二取二平臺的計算機聯(lián)鎖軟件異構性能分析及設計[J].鐵道標準設計，2016，60(11)：135-138.

[4] 曹源，唐濤，徐田華，等.形式化方法在列車運行控制系統(tǒng)中的應用[J].交通運輸工程學報，2010，10(1)：112-126.

[5] 胡雪蓮，陶彩霞.基于MSC與UPPAAL的列控系統(tǒng)等級轉(zhuǎn)換場景形式化驗證[J].鐵道標準設計，2015，59(2)：122-127.

[6] 徐世澤，肖蒙.基于Timed RAISE的高速列車RBC切換協(xié)議形式化建模及驗證[J].鐵道標準設計，2015，59(6)：138-144.

[7] 郭志良，郜春海，馬連川，等.基于時間自動機模型的安全計算機平臺的形式化驗證[J].鐵道學報，2011，33(6)：68-73.

[8] 呂繼東，唐濤，燕飛，等.基于UPPAAL的城市軌道交通CBTC區(qū)域控制子系統(tǒng)建模與驗證[J].鐵道學報，2009，32(3)：59-64.

[9] 彭大天，步兵.基于UPPAAL的FAO系統(tǒng)典型運營場景建模與驗證[J].鐵道學報，2013，35(6)：65-71.

[10] MEI M， XU ZH. W.， WANG X.， et al. Model checking-based safety verification for railway signal safety protocol-I[J]. Int. J. Computer Applications in Technology， 2013，46(3)：195-202.

[11] Mohamed Ghazel. Formalizing a subset of ERTMS/ETCS specifications for verification purposes[J]. Transportation Research Part C， 2014，42:60-75.

[12] 剛建雷，胡燕來，竇道飛，等.二乘二取二安全控制平臺開發(fā)[J].鐵道通信信號，2012，48(6)：1-4.

[13] 張新明，劉海祥，趙永清.二取二制式計算機聯(lián)鎖系統(tǒng)中的通信技術[J].中國鐵道科學，2005，26(5)：96-100.

[14] 張萍，趙陽.TYJL-III型計算機聯(lián)鎖系統(tǒng)研究[J].中國鐵路,2013(11)：21-26.

[15] 段武.計算機聯(lián)鎖系統(tǒng)[M].北京：中國鐵道出版社，2015.