需求階段的無線閉塞中心交接危險因素分析

劉金濤，李克平

(1.北京交通大學(xué) 國家軌道交通安全評估研究中心, 北京 100044；2.北京交通大學(xué) 軌道交通控制與安全國家重點實驗室，北京 100044)

無線閉塞中心RBC(Radio Block Center)作為我國CTCS-3級列車運行控制系統(tǒng)的核心子系統(tǒng)，向列車提供移動授權(quán)MA(Movement Authority)及各種靜態(tài)、動態(tài)線路信息以保障列車的安全運行。由于RBC的管轄范圍有限，在相鄰RBC之間要進(jìn)行列車控制權(quán)的交接。在RBC交接過程中出現(xiàn)任何與MA、線路信息等有關(guān)的問題，都有可能影響高速列車的正常運行，甚至導(dǎo)致高速鐵路安全事故。根據(jù)鐵路安全標(biāo)準(zhǔn)EN 50129[1]的要求，要在系統(tǒng)生命周期的需求階段對系統(tǒng)實施危險因素分析，找出可能的危險致因，以便為后續(xù)的系統(tǒng)安全設(shè)計和安全評估提供依據(jù)。因此，在需求階段對RBC交接過程進(jìn)行危險因素分析，對于保障RBC交接過程中列車的安全運行具有重要意義。

需求階段的危險因素分析是對系統(tǒng)需求規(guī)范所描述的系統(tǒng)進(jìn)行分析。由于系統(tǒng)需求規(guī)范采用不同類型的描述方式(如術(shù)語描述、結(jié)構(gòu)描述、場景描述等)從多種角度描述系統(tǒng)需求，并且不同類型的描述又相互關(guān)聯(lián)(參見《CTCS-3級列控系統(tǒng)需求規(guī)范》[2])，因此保證了系統(tǒng)需求規(guī)范的邏輯嚴(yán)密性，但也帶來了復(fù)雜的表述以及部分信息的重疊。這就要求用于危險因素分析的建模語言要具有較強(qiáng)且無二義性的表達(dá)能力。另外，從控制結(jié)構(gòu)的角度來講，RBC交接過程中存在控制-反饋回路(如RBC與車載設(shè)備、車載設(shè)備與列車等)，而控制-反饋結(jié)構(gòu)容易造成危險致因之間非線性的因果關(guān)系[3]，增加了危險因素分析的難度。

目前應(yīng)用較為廣泛的系統(tǒng)危險因素分析方法主要基于事件鏈機(jī)制，代表方法有故障樹分析FTA、失效模式影響分析FMEA等。這類方法認(rèn)為系統(tǒng)危險的出現(xiàn)是由一系列因果關(guān)系事件的順序發(fā)生所導(dǎo)致的?；谑录湹姆治龇椒ㄒ撞僮?，但是難以分析非線性因果關(guān)系的致因事件[3]。另外，此類方法受分析人員技能水平的影響較大。為此，有學(xué)者研究基于模型的危險因素分析方法[4-6]， 該方法以系統(tǒng)狀態(tài)模型或失效邏輯模型為基礎(chǔ)，例如NuSMV模型[4]、AADL模型[5]、FPTN模型[6]等，并利用形式化分析工具自動進(jìn)行致因分析，在一定程度上減少了分析人員的技能水平對于分析結(jié)果準(zhǔn)確性的影響。但是，基于模型的方法在本質(zhì)上也屬于基于事件鏈的方法，難以分析非線性因果關(guān)系的致因事件。

與前述方法不同，基于系統(tǒng)理論的事故模型及過程[3]STAMP(System-theoretic Accident Model and Processes)，以分層控制結(jié)構(gòu)作為分析模型，從控制的角度來分析安全問題。STAMP關(guān)注系統(tǒng)內(nèi)部的控制與反饋過程，能夠充分分析非線性因果關(guān)系的危險致因。因此，本文基于STAMP理論對RBC交接過程進(jìn)行危險因素分析。但是，現(xiàn)有研究[7-8]主要使用自然語言來描述分層控制結(jié)構(gòu)，容易出現(xiàn)歧義或表述模糊的情況，難以滿足需求階段危險因素分析對建模語言的要求。而且，目前基于STAMP進(jìn)行危險因素分析完全依靠分析人員進(jìn)行人工實施，分析結(jié)果可信度受分析人員技能水平的影響較大。

考慮到形式化的混成自動機(jī)[9]HA(Hybrid Automata)具有準(zhǔn)確、無二義性、可進(jìn)行圖形化建模的優(yōu)點，且對象約束語言O(shè)CL(Object Constraint Language)[10]能夠?qū)D形化模型無法表達(dá)的建模信息進(jìn)行描述，本文使用混成自動機(jī)結(jié)合OCL來描述分層控制結(jié)構(gòu)。另外，在混成自動機(jī)模型的基礎(chǔ)上，本文利用形式化的可達(dá)性分析對部分危險因素進(jìn)行自動化辨識。

1 STAMP概述

STAMP基于系統(tǒng)論的觀點認(rèn)為系統(tǒng)具有層次化的控制結(jié)構(gòu)，即系統(tǒng)由多個不同層次的控制環(huán)路組成，其中上一層的組織或結(jié)構(gòu)通過控制過程來向下一層的組織或結(jié)構(gòu)施加約束，同時下一層通過反饋過程向上一層反映約束的執(zhí)行情況。在這種層次控制過程中，如果某一層出現(xiàn)了不安全的控制，整個系統(tǒng)的安全就難以保證。文獻(xiàn)[3]給出了詳細(xì)的不安全控制分類，比如控制器向被控者發(fā)出錯誤的控制命令，控制器在必要的時候沒有提供控制命令等等。不安全的控制是系統(tǒng)事故出現(xiàn)的直接致因，而不安全控制行為則是由系統(tǒng)中的控制缺陷(如控制算法存在問題、執(zhí)行器存在問題等)導(dǎo)致的，因此控制缺陷是系統(tǒng)事故的根本致因?？刂迫毕莸囊话惴诸惪蓞⒁娢墨I(xiàn)[3]，在此不再贅述。

基于STAMP分析系統(tǒng)危險的致因，主要分為以下幾個步驟：針對已經(jīng)辨識出的系統(tǒng)危險，建立系統(tǒng)的分層控制結(jié)構(gòu)；根據(jù)分層控制結(jié)構(gòu)，找出系統(tǒng)中潛在的不安全控制；依據(jù)控制缺陷分類，進(jìn)一步分析不安全控制出現(xiàn)的原因——控制缺陷，即系統(tǒng)危險的根本致因。

2 需求階段的危險因素分析方法

基于STAMP理論，需求階段的危險因素分析方法如圖1所示，分為3步：步驟1，針對待分析的系統(tǒng)級危險，建立需求階段的危險因素分析模型，即系統(tǒng)分層控制結(jié)構(gòu)；步驟2，辨識潛在的導(dǎo)致系統(tǒng)危險的不安全控制；步驟3，依據(jù)需求階段的控制缺陷分類，通過人工分析和形式化分析相結(jié)合的方式，確定控制缺陷。

圖1 需求階段的危險因素分析方法框圖

本文提出的需求階段的危險因素分析方法與以往基于STAMP的危險因素分析過程一致，主要區(qū)別在于：在步驟1中采用分層控制框圖、混成自動機(jī)以及對象約束語言O(shè)CL實現(xiàn)系統(tǒng)分層控制結(jié)構(gòu)的刻畫，而非自然語言形式的分層控制結(jié)構(gòu)構(gòu)建方式；在步驟3中依據(jù)需求階段的控制缺陷分類實施危險因素分析，而非系統(tǒng)運行階段的控制缺陷分類；在步驟3中采用人工分析與形式化分析相結(jié)合的方式辨識控制缺陷，而非完全的人工分析方式。

2.1 危險因素分析模型構(gòu)建

根據(jù)STAMP理論，危險因素分析模型由系統(tǒng)組件間的控制反饋關(guān)系、控制器內(nèi)部的控制算法、過程模型、執(zhí)行器和傳感器的工作過程等內(nèi)容組成[2]。對此，本文采用如下建模策略分別針對不同內(nèi)容進(jìn)行建模，從而最終構(gòu)成危險因素分析模型。

(1)采用STAMP理論中的分層控制框圖[2]對RBC交接過程中各組件的關(guān)系進(jìn)行刻畫。其中，組件間的控制關(guān)系以向下的箭頭進(jìn)行表示，反饋關(guān)系以向上的箭頭進(jìn)行表示。

(2)利用混成自動機(jī)[9]對控制算法、執(zhí)行器和傳感器的工作過程進(jìn)行刻畫。其中，利用混成自動機(jī)的狀態(tài)表示控制算法的具體步驟，利用狀態(tài)遷移觸發(fā)條件表示算法各步驟的判定條件，利用混成自動機(jī)的狀態(tài)遷移過程刻畫相應(yīng)組件的動態(tài)工作過程。

(3)除了上述分層控制關(guān)系、控制算法、執(zhí)行器和傳感器之外，危險因素分析模型中還包含控制器的過程模型。過程模型是控制器對被控過程的理解和認(rèn)知，例如，在RBC交接過程中RBC的過程模型就是列車當(dāng)前狀態(tài)、周圍環(huán)境等信息的集合。

根據(jù)STAMP理論對于過程模型的描述，本文給出過程模型的形式化定義如下。

定義1控制器中的過程模型PM(Process Model)是一個五元組，PM= (S,E,f,R,W)，其中：

(1)S={Si,i=1, 2, …,N}是一個非空有限的系統(tǒng)變量集合，N為被控對象的系統(tǒng)變量總個數(shù),Si為被控對象的第i個系統(tǒng)變量。

(2)E={Ej,j=1, 2, …,M}是一個非空有限的環(huán)境變量集合，M為被控對象所處環(huán)境的環(huán)境變量總數(shù),Ej為被控對象的第j個環(huán)境變量。

(3)f：S→{S,E}為變量集合之間的關(guān)系函數(shù)，且f={fS,fE}，fS為系統(tǒng)變量之間的關(guān)系函數(shù)，fE為系統(tǒng)變量與環(huán)境變量之間的關(guān)系函數(shù)。

(4)R={fS(Si,Sk) ,fE(Sl,Ej)}是變量之間的關(guān)系集合，其中，{Si,Sk,Sl,i≠k}?S且Ej∈E。

(5)W={Wp(Si) ,Si∈S,p=1, 2, …,V}是改變被控對象狀態(tài)的行為集合，其自變量為被控對象的系統(tǒng)變量。

根據(jù)上述過程模型的定義，過程模型主要包含系統(tǒng)變量、環(huán)境變量、變量間的關(guān)系以及改變系統(tǒng)狀態(tài)的方式等內(nèi)容。對此，本文采用對象約束語言O(shè)CL[10]分別對各項內(nèi)容進(jìn)行描述。

2.2 需求階段的控制缺陷分類

建立系統(tǒng)的危險因素分析模型之后，可辨識系統(tǒng)中潛在的不安全控制。這些不安全控制是系統(tǒng)危險的直接致因，而導(dǎo)致不安全控制的控制缺陷才是危險的根本致因。在此，需要依據(jù)一定的控制缺陷分類作為指導(dǎo)原則辨識控制缺陷。

雖然STAMP給出了控制缺陷的一般性分類[3]，但是這些控制缺陷反映的是系統(tǒng)實際運行中的危險因素，例如，不恰當(dāng)?shù)膱?zhí)行器操作會導(dǎo)致控制行為的錯誤實施；錯誤的修改控制算法會造成錯誤的控制行為等。需求階段的系統(tǒng)由系統(tǒng)需求規(guī)范SRS(System Requirements Specification)來描述，反映的是需求層面的系統(tǒng)結(jié)構(gòu)、工作流程等信息，因而此階段的控制缺陷將有不同的表現(xiàn)形式。

為了明確需求階段的控制缺陷分類，本文定義了影響控制行為的因素集合。

定義2控制器的控制行為CA(Control Action)受五元組(AL，PM，C，A，F(xiàn))的影響表示為

(AL，PM，C，A，F(xiàn))→CA

( 1 )

式中：AL表示控制器的控制算法，在需求階段，AL由系統(tǒng)需求規(guī)范進(jìn)行描述，并且通過控制器中的功能模塊來具體實現(xiàn)；PM表示控制器中的過程模型，在需求階段，PM由系統(tǒng)需求規(guī)范進(jìn)行定義，同時其變量的初始值由控制器的輸入決定；C表示控制器的協(xié)作關(guān)系，控制器各自的責(zé)任及與其他控制器的關(guān)系由系統(tǒng)需求規(guī)范進(jìn)行定義說明；A表示控制環(huán)路中的執(zhí)行器，在需求階段，A的功能由系統(tǒng)需求規(guī)范進(jìn)行描述，并且通過其內(nèi)部功能模塊來具體實現(xiàn)；F表示控制環(huán)路中的反饋過程，反饋機(jī)制由系統(tǒng)需求規(guī)范進(jìn)行定義，并且通過傳感器的內(nèi)部功能模塊具體實現(xiàn)。

根據(jù)上述定義可以看出，影響控制行為的各類因素在需求階段主要由以下3方面內(nèi)容決定：控制器的輸入、控制環(huán)路中各個組件的功能模塊以及系統(tǒng)需求規(guī)范的描述。如果這3方面內(nèi)容出現(xiàn)問題，定義2中的5類元素就會相應(yīng)出現(xiàn)問題，進(jìn)而導(dǎo)致不安全的控制行為。根據(jù)定義2中的內(nèi)容，得到需求階段控制缺陷的一般性分類，如圖2所示。

圖2 需求階段的控制缺陷分類

圖2給出的控制缺陷分類主要面向系統(tǒng)需求階段。根據(jù)控制缺陷不同的來源，圖2所示的控制缺陷可分為：與控制器輸入相關(guān)的控制缺陷、與組件功能模塊相關(guān)的控制缺陷以及與系統(tǒng)需求規(guī)范相關(guān)的控制缺陷。后續(xù)的危險因素分析將依據(jù)這種控制缺陷分類來展開。

2.3 控制缺陷分析

根據(jù)需求階段的控制缺陷分類，可分析造成不安全控制的原因，即系統(tǒng)危險的根本致因。本文采用人工分析和形式化分析相結(jié)合的方式來辨識控制缺陷，如圖3所示。

圖3 控制缺陷分析方法框圖

圖3左邊虛線框表示通過人工分析的方式，辨識與控制器輸入相關(guān)的控制缺陷。其中，主要依據(jù)“控制器的輸入錯誤、缺失或沒有及時更新”作為引導(dǎo)詞，對該類控制缺陷進(jìn)行辨識。

圖3右邊虛線框表示利用可達(dá)性分析[11]，辨識與組件功能模塊相關(guān)以及與系統(tǒng)需求規(guī)范相關(guān)的控制缺陷，包括：

(1)根據(jù)危險因素分析模型中的混成自動機(jī)模型，建立形式化工具可執(zhí)行的PHAVer模型。

(2)基于形式化的PHAVer模型，將不安全控制作為目標(biāo)集合進(jìn)行可達(dá)性分析。如果目標(biāo)集合可達(dá)，則根據(jù)工具給出的系統(tǒng)可達(dá)集合逆向確認(rèn)與系統(tǒng)需求規(guī)范SRS相關(guān)的控制缺陷；如果目標(biāo)集合不可達(dá)，則不存在該類控制缺陷。

(3)基于形式化的PHAVer模型，利用故障注入的方式對其進(jìn)行擴(kuò)展。利用擴(kuò)展后的模型，進(jìn)行可達(dá)性分析，辨識與組件功能模塊相關(guān)的控制缺陷。對于該過程的具體實現(xiàn)，可詳見文獻(xiàn)[12]。

3 需求階段的RBC交接建模與分析

3.1 RBC交接場景及系統(tǒng)危險

在CTCS-3級系統(tǒng)中，列車車載設(shè)備向RBC報告列車當(dāng)前的位置等信息，并接收由RBC提供的移動授權(quán)MA(Movement Authority)。由于RBC的管轄范圍有限，列車從當(dāng)前RBC(移交RBC)管轄區(qū)域行駛至相鄰RBC(接收RBC)管轄區(qū)域時，列車控制權(quán)要進(jìn)行相應(yīng)的交接，為此《CTCS-3級系統(tǒng)需求規(guī)范》[2]規(guī)定了詳細(xì)的流程，這個過程稱之為RBC交接。RBC交接過程可根據(jù)列車車載電臺的工作情況分為：只有一部電臺正常的RBC交接和兩部電臺都正常的RBC交接。本文僅考慮兩部電臺同時工作的RBC交接過程。

在兩部電臺都正常的情況下，當(dāng)列車通過RBC切換預(yù)告應(yīng)答器組后，車載設(shè)備向“移交RBC”發(fā)送列車位置報告。“移交RBC”接收到位置報告后，向列車及“接收RBC”發(fā)送相應(yīng)信息，從而正式發(fā)起交接過程。一方面，“移交RBC”根據(jù)“接收RBC”提供的信息，生成包含邊界的MA并發(fā)送給列車；另一方面，列車與“接收RBC”建立會話。當(dāng)列車的最大安全前端通過交接邊界后，“接收RBC”將接管列車控制權(quán)并通知“移交RBC”。當(dāng)列車最小安全末端經(jīng)過邊界應(yīng)答器組后，列車與“移交RBC”最終結(jié)束會話。詳細(xì)的交接流程可參見文獻(xiàn)[12]。

另外，本文選取“在RBC交接過程中，CTCS-3級列控系統(tǒng)未能防止列車超出安全的速度及距離限制”作為待分析的系統(tǒng)級危險。

3.2 危險因素分析模型

圖4 RBC交接過程的分層控制框圖

根據(jù)前述內(nèi)容，首先建立系統(tǒng)的分層控制框圖，如圖4所示。圖4給出了RBC交接過程的系統(tǒng)分層控制框圖。其中，Handover RBC表示移交RBC；Takeover RBC表示接收RBC；OBE表示車載設(shè)備；Train表示列車。圖4中向下的箭頭表示控制，例如車載設(shè)備控制列車；向上的箭頭表示反饋，例如列車向車載設(shè)備反饋當(dāng)前速度；水平箭頭表示控制器之間的信息交互，例如“移交RBC”與“接收RBC”之間存在信息交互。圖4中箭頭旁的信息表示相應(yīng)的控制命令、反饋數(shù)據(jù)或交互信息，其具體含義見表1。

在圖4所示的分層控制結(jié)構(gòu)中，兩個RBC以及車載設(shè)備作為控制器，具有控制算法和過程模型。針對各自的控制算法以及列車的運行過程，建立相應(yīng)的混成自動機(jī)模型，如圖5所示。

表1 圖4中信息的含義

圖5 RBC交接過程的混成自動機(jī)模型

圖5(a)給出了RBC交接過程中車載設(shè)備的混成自動機(jī)模型。其中，該模型由并發(fā)的上下兩個自動機(jī)模型組成。上部的模型僅有一個通信狀態(tài)Comm，表示車載設(shè)備與RBC的通信過程，包含發(fā)送位置報告、接收通信版本信息等；下部的模型主要描述車載設(shè)備對列車的監(jiān)控算法，包括曲線計算CurveCal、監(jiān)控Supervision、報警Warning、常用制動觸發(fā)ServiceBrake、緊急制動觸發(fā)EmergBrake等狀態(tài)，車載設(shè)備首先計算速度監(jiān)控曲線，然后進(jìn)行速度比較，最后根據(jù)相應(yīng)的結(jié)果選擇實施報警、常用制動或緊急制動。

圖5(b)所示混成自動機(jī)模型描述了交接過程中列車的運行狀態(tài)，包括加速Acc、減速Dec、常用制動SBrake以及緊急制動EBrake。其中，關(guān)鍵字flow所引導(dǎo)的微分表達(dá)式描述了列車的動態(tài)行駛過程，不變集inv對列車的速度、加速度取值進(jìn)行了約束。常數(shù)A和-B分別代表列車的最大加速度和最大減速度，mV和k分別代表期望速度值和實際偏差值。

圖5(c)給出了RBC交接過程中“移交RBC”和“接收RBC”的混成自動機(jī)模型，該模型由并發(fā)的上中下3個自動機(jī)模型組成。上部的模型描述了“移交RBC”的移交控制算法，包括起始Initial-a、消息處理Handle-a、預(yù)移交PreHand以及移交Handover等4個過程。中部模型描述了“接收RBC”的接管控制算法，包括起始Initial-b、消息處理Handle-b以及接管Takeover等3個過程。最下部的模型描述了“移交RBC”和“接收RBC”對列車的控制算法，包括列車管理TrainManage、進(jìn)路檢查RouteCheck、移動授權(quán)縮短MAShorten、移動授權(quán)計算MACalculate和消息發(fā)送MesgSend等過程。圖5中的消息含義參見表1。

根據(jù)定義1，建立RBC和車載設(shè)備的過程模型，如圖6、圖7所示。其中，圖6所示的過程模型同屬于“移交RBC”和“接收RBC”，對RBC中的列車位置、進(jìn)路情況等變量進(jìn)行聲明，并刻畫了各變量間的約束關(guān)系，例如進(jìn)路的取消將導(dǎo)致MA的縮短等。另外，還對改變變量取值的方式進(jìn)行了描述。圖7所示過程模型對車載設(shè)備中列車速度、列車位置、MA終點等變量進(jìn)行了聲明，給出了變量間的約束關(guān)系，例如列車制動距離不能超過MA終點等。此外，還描述了車載設(shè)備改變列車狀態(tài)的方式，如常用制動、緊急制動等。

圖6 RBC的過程模型

圖7 車載設(shè)備的過程模型

3.3 系統(tǒng)危險致因分析

根據(jù)圖1所示方法，步驟2和步驟3要分析系統(tǒng)危險的致因。其中，步驟2辨識不安全控制，步驟3辨識導(dǎo)致不安全控制的控制缺陷。

3.3.1 不安全的控制

根據(jù)圖4給出的控制框圖，辨識出導(dǎo)致系統(tǒng)級危險“在RBC交接過程中，CTCS-3級列控系統(tǒng)未能防止列車超出安全的速度及距離限制”的不安全控制UCA(Unsafe Control Action)如下：

UCA1：在RBC交接過程中，“移交RBC”向車載設(shè)備提供了錯誤的包含交接邊界的MA。

UCA2：列車接近交接邊界且“接收RBC”轄區(qū)內(nèi)進(jìn)路發(fā)生變化時，“移交RBC”未及時縮短MA。

UCA3：存在臨時限速時，“移交RBC”沒有向車載設(shè)備提供臨時限速。

UCA4：存在臨時限速時，“移交RBC”提供了錯誤的臨時限速。

UCA5：當(dāng)需要車載設(shè)備實施制動時，車載設(shè)備沒有提供制動命令。

3.3.2 控制缺陷分析

對于與控制器輸入相關(guān)的控制缺陷ICF(Input- related Control Flaws)，以圖2所示的“控制器的輸入錯誤、缺失或者沒有及時更新”作為引導(dǎo)詞，并結(jié)合圖6、圖7所示過程模型，進(jìn)行人工分析，結(jié)果如下：

UCA1：在RBC交接過程中，“移交RBC”向車載設(shè)備提供了錯誤的包含交接邊界的MA。

ICF1.1：“接收RBC”向“移交RBC”提供的轄區(qū)內(nèi)進(jìn)路信息錯誤；

ICF1.2：“移交RBC”獲得錯誤的列車位置；

ICF1.3：“移交RBC”獲得錯誤的列車數(shù)據(jù)。

UCA2：列車接近交接邊界且“接收RBC”轄區(qū)內(nèi)進(jìn)路發(fā)生變化時，“移交RBC”未及時縮短MA。

ICF2.1：“接收RBC”沒有及時向“移交RBC”提供新的進(jìn)路信息；

ICF2.2：“移交RBC”中的列車位置更新不及時。

UCA3：存在臨時限速時，“移交RBC”沒有向車載設(shè)備提供臨時限速。

ICF3.1：“移交RBC”未收到臨時限速；

ICF3.2：“移交RBC”收到的臨時限速設(shè)置范圍錯誤。

UCA4：存在臨時限速時，“移交RBC”提供了錯誤的臨時限速。

ICF4.1：“移交RBC”收到的臨時限速錯誤。

UCA5：當(dāng)需要車載設(shè)備實施制動時，車載設(shè)備沒有提供制動命令。

ICF5.1：車載設(shè)備獲得錯誤的列車實際速度；

ICF5.2：車載設(shè)備中用于計算速度距離曲線的列車數(shù)據(jù)錯誤；

ICF5.3：車載設(shè)備獲得錯誤的線路描述數(shù)據(jù)；

ICF5.4：車載設(shè)備獲得錯誤的MA信息。

對于與組件功能模塊相關(guān)的控制缺陷以及與系統(tǒng)需求規(guī)范相關(guān)的控制缺陷，利用形式化的方式進(jìn)行辨識。

首先，將圖5所示的混成自動機(jī)模型轉(zhuǎn)換為形式化工具可執(zhí)行的PHAVer模型，限于篇幅，模型片段如圖8所示。

圖8 PHAVer模型片段

其次，將不安全控制描述為目標(biāo)集合的形式，見表2。利用形式化工具PHAVer對模型進(jìn)行可達(dá)性分析。結(jié)果顯示目標(biāo)集合不可達(dá)，說明不存在與系統(tǒng)需求規(guī)范相關(guān)的控制缺陷。

表2 不安全控制及相應(yīng)的功能相關(guān)控制缺陷

最后，根據(jù)經(jīng)驗并參考文獻(xiàn)[13]所列舉的組件功能故障情況，選取48個與車載設(shè)備及RBC相關(guān)的故障進(jìn)行故障注入，即在系統(tǒng)PHAVer模型中增加故障情況下的狀態(tài)遷移，構(gòu)成擴(kuò)展后的形式化模型。同樣以表2所示的不安控制為目標(biāo)集合，利用形式化工具PHAVer對擴(kuò)展后的模型進(jìn)行可達(dá)性分析。結(jié)果顯示目標(biāo)集合可達(dá)，即注入故障之后，系統(tǒng)中將會出現(xiàn)不安全控制。根據(jù)形式化工具給出的可達(dá)狀態(tài)集合，可確定與組件功能模塊相關(guān)的控制缺陷，見表2。其中，表2中功能模塊故障含義見表3。

表3 功能模塊故障的含義

表3(續(xù))

3.4 與現(xiàn)有研究的比較

文獻(xiàn)[13-14]采用傳統(tǒng)的FTA和FMEA對需求階段的ETCS-2級列控系統(tǒng)RBC交接進(jìn)行了危險致因分析。將上述文獻(xiàn)與本文工作進(jìn)行比較后發(fā)現(xiàn)：

(1)上述文獻(xiàn)對于與輸入相關(guān)的危險致因描述并不詳細(xì)。例如，文獻(xiàn)[13]將“不正確的地面子系統(tǒng)輸入數(shù)據(jù)”作為危險致因，并沒有描述不正確輸入的相關(guān)詳細(xì)內(nèi)容。而詳細(xì)的致因信息是后續(xù)系統(tǒng)安全設(shè)計和安全評估的重要依據(jù)。相比之下，本文分析與輸入相關(guān)的控制缺陷時，不僅明確了是哪些不正確的輸入導(dǎo)致危險，還指出了不正確輸入的類型(錯誤、缺失或者更新不及時)，比如，RBC獲取的限速信息錯誤、RBC中的列車位置更新不及時等。造成這種差異的原因在于：故障樹本身不含有引導(dǎo)詞，其分析的細(xì)致程度更多的是由分析人員的主觀經(jīng)驗來決定。而本文使用了不安全控制分類、需求階段控制缺陷分類等起引導(dǎo)詞作用的信息，有助于更細(xì)致的分析。

(2)當(dāng)針對不同的系統(tǒng)危險進(jìn)行分析時，文獻(xiàn)[13-14]的分析過程重用性較差。而本文所建的分層控制框圖、混成自動機(jī)模型以及過程模型可重復(fù)用于不同危險的分析。

除上述基于FTA、FMEA的危險因素分析外，文獻(xiàn)[4-5]采用基于形式化模型的方式來分析系統(tǒng)危險因素。利用形式化模型(如SMV模型、AADL模型等)描述系統(tǒng)狀態(tài)，通過故障注入的方式將系統(tǒng)組件的功能故障添加至形式化模型，利用模型檢驗的方式分析系統(tǒng)危險致因。然而，這些形式化的分析方法采用故障注入的方式，難以分析除組件功能故障之外的危險致因。相比之下，本文利用人工分析與形式化分析相結(jié)合的方式既能分析與組件功能相關(guān)的致因，又能分析與組件輸入相關(guān)的致因。另外，文獻(xiàn)[4-5]采用模型檢驗技術(shù)進(jìn)行危險因素分析，當(dāng)系統(tǒng)變量較多時易出現(xiàn)“狀態(tài)空間爆炸”的問題。而本文所采用的可達(dá)性分析技術(shù)則不存在此類問題。

4 結(jié)束語

本文采用分層控制框圖刻畫RBC交接過程中的控制-反饋關(guān)系，并利用混成自動機(jī)HA和對象約束語言O(shè)CL分別描述其中的控制算法、過程模型等內(nèi)容，實現(xiàn)對需求階段RBC交接分層控制結(jié)構(gòu)的刻畫。針對RBC交接過程中具體的系統(tǒng)危險，依據(jù)需求階段的控制缺陷分類，利用人工分析和形式化分析相結(jié)合的方式辨識系統(tǒng)危險的根本致因。將分析結(jié)果與現(xiàn)有研究結(jié)果進(jìn)行比較，結(jié)果表明本文所提方法適用于需求階段的RBC交接危險因素分析。

參考文獻(xiàn)：

[1]CENELEC. Standard EN 50129 Railway Applications: Communications, Signaling and Processing Systems Safety Related Electronic Systems for Signaling [S]. 2003.

[2]中華人民共和國鐵道部. CTCS-3級列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS) [S]. 北京：中國鐵道出版社，2009.

[3]LEVESON N G. Engineering a Safer World: Systems Thinking Applied to Safety Engineering Systems [M]. Massachusetts: MIT Press, 2012.

[4]VILLAFIORITA A. The FSAP/NuSMV-SA Safety Analysis Platform [J]. International Journal on Software Tools for Technology Transfer， 2007, 9(1):5-24.

[5]BOZZANO M. Safety, Dependability and Performance Analysis of Extended AADL Models [J]. The Computer Journal, 2010, 54(5):1-22.

[6]RU N, TAO T. A Model-based Framework for the Safety Analysis of Computer-based Railway Signaling Systems [C]// Computer System Design and Operation in the Railway and other Transit Systems， 2010, 114: 827-838.

[7]ISHIMATSU T. Hazard Analysis of Complex Spacecraft Using Systems-theoretic Process Analysis [J]. Journal of Spacecraft & Rockets, 2014, 51(2):509-522.

[8]LU Y Z, SHU G T. STAMP-based Safety Control Approach for Flight Testing of a Low-cost Unmanned Subscale Blended-wing-body Demonstrator [J]. Safety Science, 2015, 74:102-113.

[9]THOMAS A, HENZINGER Z. The Theory of Hybrid Automata [C]// Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. New York: IEEE,1996： 278-292.

[10]CORREA A, WERNER C, BARROS M. Refactoring to Improve the Understandability of Specifications Written in Object Constraint Language [J]. IET Software， 2009, 3(2): 69-90.

[11]DANG T, TESTYLIER R. Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion [J]. Reliable Computing, 2013:128-152.

[12]劉金濤，唐濤，趙林，等. 基于UML模型的CTCS-3級列控系統(tǒng)功能安全分析方法[J]. 鐵道學(xué)報, 2013, 35(10):59-66.

LIU Jintao, TANG Tao, ZHAO Lin, et al. Functional Safety Analysis of CTCS-3 Train Control System Based on

UML Model [J]. Journal of the Railway Society, 2013, 35(10):59-66.

[13]ERTMS/ETCS SUBSET-088: ETCS Application Level 2- Safety Analysis Part 1-Functional Fault Tree [EB/OL]. http://www.era.europa.eu.2016-08-01.

[14]ERTMS/ETCS SUBSET-078: Failure Modes and Effects Analysis for ETCS Application Level 2 [EB/OL]. http://www.era.europa.eu.2016-08-01.