劉振宇，李 晶

（北京城建設(shè)計(jì)發(fā)展集團(tuán)股份有限公司，北京 100045）

隨著軌道交通行業(yè)的快速發(fā)展，傳統(tǒng)列控系統(tǒng)暴露出一系列弊端，例如客運(yùn)壓力大、行車(chē)效率低、軌旁設(shè)備繁多等[1]。眾多科研機(jī)構(gòu)和企業(yè)積極進(jìn)行新一代列控系統(tǒng)的開(kāi)發(fā)，對(duì)列控系統(tǒng)的結(jié)構(gòu)與功能進(jìn)行進(jìn)一步優(yōu)化。

通過(guò)分析國(guó)外列控的發(fā)展趨勢(shì)，結(jié)合中國(guó)列控技術(shù)的現(xiàn)狀，北京交通大學(xué)開(kāi)展了下一代列控系統(tǒng)技術(shù)方案研究[2]，提出基于車(chē)車(chē)通信的下一代列車(chē)運(yùn)行控制系統(tǒng)[3]。目前基于車(chē)車(chē)通信的列控系統(tǒng)尚處于研究開(kāi)發(fā)階段，有必要對(duì)列控系統(tǒng)進(jìn)行安全分析和風(fēng)險(xiǎn)評(píng)估，以確定在具體的應(yīng)用場(chǎng)景中是否存在不安全因素。由于列控系統(tǒng)是非常復(fù)雜的，相較于其他安全分析方法，STPA (system theoretic process analysis，系統(tǒng)理論過(guò)程分析方法)能夠充分考慮組件間的交互對(duì)列控系統(tǒng)安全的影響[4]，現(xiàn)使用系統(tǒng)理論過(guò)程分析方法分析列控系統(tǒng)的安全性。

本文重點(diǎn)對(duì)基于車(chē)車(chē)通信列控系統(tǒng)的 RMU(resource management unit，資源管理單元)進(jìn)行安全性分析。以RMU發(fā)送TSR (temporary speed restriction，臨時(shí)限速)場(chǎng)景為例，構(gòu)建了列控系統(tǒng)的分層控制結(jié)構(gòu)。根據(jù)列控系統(tǒng)的控制結(jié)構(gòu)，判斷該過(guò)程中危險(xiǎn)控制行為并找到控制缺陷。利用控制缺陷得到相關(guān)SDR(security design requirements，安全性設(shè)計(jì)需求)。通過(guò)UPPAAL工具搭建TSR發(fā)送場(chǎng)景下的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，最后把SDR翻譯為UPPAAL可識(shí)別的語(yǔ)言，以此來(lái)驗(yàn)證SDR的合理性。

1 基于車(chē)車(chē)通信的下一代列控系統(tǒng)介紹

基于車(chē)車(chē)通信的列控系統(tǒng)的系統(tǒng)結(jié)構(gòu)可以分為 3層，分別為：運(yùn)營(yíng)控制層、車(chē)載控制層以及軌旁控制層，如圖1所示。運(yùn)營(yíng)控制層主要由DCD (dynamic capacity decision，動(dòng)態(tài)運(yùn)能決策系統(tǒng))和RMU構(gòu)成。動(dòng)態(tài)運(yùn)能決策系統(tǒng)的功能是發(fā)送行車(chē)計(jì)劃和調(diào)度命令。RMU主要負(fù)責(zé)在線(xiàn)列車(chē)管理與臨時(shí)限速下發(fā)。車(chē)載控制層是整個(gè)列控系統(tǒng)的核心，主要由VCM (vital computer management，車(chē)載列車(chē)管理)和 VCI (vital computer interlocking，車(chē)載聯(lián)鎖)組成，具有完成移動(dòng)授權(quán)計(jì)算、列車(chē)超速防護(hù)和進(jìn)路排列等功能；軌旁控制層主要由OC (object controller，對(duì)象控制單元)等設(shè)備組成，具有信號(hào)機(jī)、轉(zhuǎn)轍機(jī)等軌旁設(shè)備的控制和表示功能。

圖1 基于車(chē)車(chē)通信列控系統(tǒng)的系統(tǒng)結(jié)構(gòu)Figure 1 Structure of train control system based on vehicle-vehicle communications

RMU作為基于車(chē)車(chē)通信列控系統(tǒng)的核心地面設(shè)備，主要功能有：①在線(xiàn)列車(chē)管理，包括列車(chē)的注冊(cè)與注銷(xiāo)；②下發(fā)臨時(shí)限速，同時(shí)接收列車(chē)運(yùn)行狀態(tài)信息匯報(bào)給DCD；③OC狀態(tài)監(jiān)督；④存儲(chǔ)與轉(zhuǎn)發(fā)列車(chē)的各種狀態(tài)數(shù)據(jù)；⑤向列車(chē)發(fā)送管轄范圍內(nèi)列車(chē)位置，輔助車(chē)載實(shí)現(xiàn)前車(chē)識(shí)別和聯(lián)鎖功能。RMU外部設(shè)備交互圖如圖2所示，由于RMU對(duì)外交互設(shè)備繁多，交互過(guò)程中極有可能出現(xiàn)故障導(dǎo)致事故發(fā)生。對(duì)其進(jìn)行安全分析和風(fēng)險(xiǎn)評(píng)估，以確定特定應(yīng)用場(chǎng)景中的不安全因素，同時(shí)制定相關(guān)的安全約束是十分必要的。

圖2 RMU對(duì)外設(shè)備交互圖Figure 2 Diagram of external device interaction

2 研究方法介紹

2.1 STPA模型概述

STAMP模型是基于系統(tǒng)理論的事故分析模型，它重點(diǎn)關(guān)注系統(tǒng)組件間的交互及控制機(jī)制[5]。STAMP理論采用多層次的系統(tǒng)結(jié)構(gòu)來(lái)表征系統(tǒng)內(nèi)部單元之間的信息流，主要是控制命令和反饋結(jié)果的。系統(tǒng)安全的重點(diǎn)由防止組件失效轉(zhuǎn)換為實(shí)施行為的安全約束，將安全問(wèn)題轉(zhuǎn)換為控制問(wèn)題而不是可靠性問(wèn)題[6]。STAMP已經(jīng)成功應(yīng)用于多種安全苛求系統(tǒng)的分析，涉及航空航天、國(guó)防工業(yè)、交通運(yùn)輸、化學(xué)工業(yè)和醫(yī)藥生成等多個(gè)領(lǐng)域[7]。

STPA基于STAMP理論構(gòu)建的系統(tǒng)控制圖進(jìn)行分析，從外部輸入開(kāi)始針對(duì)控制回路的每一個(gè)環(huán)節(jié)進(jìn)行分析，辨識(shí)致因因素。STPA以系統(tǒng)級(jí)危險(xiǎn)作為輸入，主要通過(guò)以下4個(gè)步驟辨識(shí)導(dǎo)致危險(xiǎn)出現(xiàn)的根本原因[8]：

第1步：針對(duì)系統(tǒng)級(jí)危險(xiǎn)，確立安全約束；

第2步：搭建多層次的系統(tǒng)結(jié)構(gòu)。搭建多層次的系統(tǒng)結(jié)構(gòu)，可以研究系統(tǒng)內(nèi)部各層次信息流動(dòng)的過(guò)程，從交互過(guò)程中尋找系統(tǒng)中存在的不安全因素。

第3步：尋找導(dǎo)致系統(tǒng)危險(xiǎn)的原因。針對(duì)所建立的分層控制結(jié)構(gòu)圖中的控制行為，辨識(shí)以下不安全控制行為：①系統(tǒng)發(fā)出的未定義安全要求的控制或不符合安全約束控制；②提供不安全的控制從而導(dǎo)致危險(xiǎn)；③控制行為本身是安全的但時(shí)序不正確；④系統(tǒng)進(jìn)行控制的時(shí)間不合要求。

第4步：分辨控制缺陷。該步驟需要對(duì)系統(tǒng)的各個(gè)控制閉環(huán)中的各單元進(jìn)行研究，從而分辨出系統(tǒng)的控制缺陷，如圖3所示。

圖3 控制缺陷分類(lèi)Figure 3 Classification of unsafe factors

2.2 UPPAAL 和時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)是在有限自動(dòng)機(jī)的基礎(chǔ)上添加了時(shí)間約束產(chǎn)生的[9]，可以有效地對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行建模和驗(yàn)證[10]，基于車(chē)車(chē)通信的列控系統(tǒng)是實(shí)時(shí)系統(tǒng)。

UPPAAL是一個(gè)對(duì)實(shí)時(shí)系統(tǒng)建模和驗(yàn)證的工具[11]，為實(shí)時(shí)系統(tǒng)的模型驗(yàn)證提供了一種規(guī)范化的驗(yàn)證語(yǔ)法-BNF(Backus-Naur Form，巴科斯范式)語(yǔ)法[12]，其規(guī)則如下：

3 TSR下發(fā)場(chǎng)景的安全性分析

考慮到不同場(chǎng)景下的事故會(huì)由不同的因素造成。以資源管理單元RMU向VCM下發(fā)臨時(shí)限速為例，采用STPA方法進(jìn)行安全性分析，目的是識(shí)別場(chǎng)景中的危害和不安全控制行為，以便設(shè)計(jì)安全性約束消除危害。

3.1 TSR下發(fā)場(chǎng)景介紹

臨時(shí)限速命令具有為列車(chē)提供安全防護(hù)和運(yùn)行調(diào)整的功能。TSR下發(fā)的第一步人工輸入 TSR參數(shù)，DCD接收到參數(shù)后生成臨時(shí)限速命令，經(jīng)過(guò)相關(guān)協(xié)議拆分和轉(zhuǎn)換后發(fā)送給相關(guān)RMU進(jìn)行有效性驗(yàn)證。TSR檢驗(yàn)無(wú)誤后進(jìn)行保存并等待執(zhí)行，如果有效性驗(yàn)證失敗，通過(guò)提示，值班員可在調(diào)整TSR參數(shù)后再次發(fā)送命令。RMU驗(yàn)證成功后，將TSR命令發(fā)送給管轄范圍內(nèi)的列車(chē)，VCM接收到TSR后，執(zhí)行臨時(shí)限速命令，然后向RMU發(fā)送反饋信息。

3.2 基于STPA的TSR下發(fā)場(chǎng)景安全分析

3.2.1 定義系統(tǒng)級(jí)危險(xiǎn)及安全約束

由相關(guān)標(biāo)準(zhǔn)和規(guī)范可以得到列控系統(tǒng)的系統(tǒng)級(jí)危險(xiǎn)：列車(chē)速度大于安全速度或者超出安全距離限制，標(biāo)記為“H1”作為要分析的系統(tǒng)級(jí)危險(xiǎn)，針對(duì)該系統(tǒng)級(jí)危險(xiǎn)，安全條件是列車(chē)運(yùn)行控制系統(tǒng)必須保證列車(chē)運(yùn)行速度不超過(guò)安全速度或超出安全距離限制。

3.2.2 建立待分析系統(tǒng)的分層控制結(jié)構(gòu)

使用分層框圖對(duì)基于車(chē)車(chē)通信列控系統(tǒng)的分層控制結(jié)構(gòu)進(jìn)行描述。分層控制結(jié)構(gòu)不僅包括列控子系統(tǒng)(例如 RMU，DCD 等)，也包括調(diào)度員以及司機(jī)等。圖4為RMU向VCM發(fā)送臨時(shí)限速命令的分層控制結(jié)構(gòu)圖，圖中實(shí)線(xiàn)框內(nèi)為基于車(chē)車(chē)通信的列控系統(tǒng)內(nèi)部包含的單元，虛線(xiàn)框內(nèi)為列控系統(tǒng)外部單元。

圖4 分層控制結(jié)構(gòu)Figure 4 Hierarchical control structure

在構(gòu)建分層控制結(jié)構(gòu)圖之后，可以細(xì)化系統(tǒng)的交互過(guò)程，得到過(guò)程模型，如圖5所示。過(guò)程模型是控制器對(duì)被控過(guò)程的理解和認(rèn)知[13]，控制器中的相關(guān)算法也是在此基礎(chǔ)上形成的。

圖5 過(guò)程模型Figure 5 Process model

3.2.3 不安全控制行為辨識(shí)

根據(jù)基于車(chē)車(chē)通信的列控系統(tǒng)在臨時(shí)限速下發(fā)場(chǎng)景中的控制行為，針對(duì)危險(xiǎn)H1，辨識(shí)出可能的不安全控制行為，表1為部分不安全控制行為。

表1 不安全控制行為T(mén)able 1 Unsafe control behavior

3.2.4 控制缺陷分析

最后需要研究列控系統(tǒng)的控制缺陷，找到不安全控制場(chǎng)景出現(xiàn)的因素。TSR下發(fā)場(chǎng)景中的不安全因素如圖6所示。

圖6 TSR下發(fā)場(chǎng)景中的不安全因素Figure 6 Unsafe factors in TSR sending scenarios

控制缺陷如下：

CD1：調(diào)度員疏忽，忘記下達(dá)臨時(shí)限速命令。

CD2：調(diào)度員疏忽，過(guò)晚的下達(dá)臨時(shí)限速命令。

CD3：調(diào)度員操作不當(dāng)，下達(dá)錯(cuò)誤的臨時(shí)限速命令。

CD4：DCD未接受到調(diào)度員操作命令，或收到錯(cuò)誤的命令，過(guò)晚收到命令。

CD5：DCD自身硬件出現(xiàn)故障。

CD6：DCD的算法設(shè)計(jì)存在缺陷。

CD7：DCD未向RMU下達(dá)臨時(shí)限速。

CD8：DCD對(duì)TSR的解析出現(xiàn)錯(cuò)誤。

CD9：DCD過(guò)晚地向RMU下達(dá)臨時(shí)限速信息。

CD10：RMU未收到來(lái)自DCD的TSR，或收到錯(cuò)誤的TSR，超時(shí)收到TSR。

CD11：RMU自身硬件出現(xiàn)故障。

CD12：RMU的算法設(shè)計(jì)存在缺陷。

CD13：RMU未向VCM下達(dá)臨時(shí)限速。

CD14：RMU解析TSR出現(xiàn)錯(cuò)誤。

CD15：RMU過(guò)晚地向VCM下達(dá)臨時(shí)限速信息

CD16：VCM未收到來(lái)自RMU的TSR，或收到錯(cuò)誤的TSR，超時(shí)收到TSR。

CD17：VCM對(duì)TSR解析錯(cuò)誤。

CD18：VCM自身硬件出現(xiàn)故障。

CD19：VCM的算法設(shè)計(jì)存在缺陷。

CD20：速度傳感器速度測(cè)量誤差過(guò)大。

3.2.5 安全性設(shè)計(jì)需求

對(duì)所得的控制缺陷進(jìn)行分析，制定出相應(yīng)的安全性設(shè)計(jì)需求，為UPPAAL模型驗(yàn)證語(yǔ)句提供來(lái)源。部分與RMU相關(guān)的安全性設(shè)計(jì)需求如下：

SDR1：RMU必須進(jìn)行冗余和可靠性設(shè)計(jì)。

SDR2：RMU系統(tǒng)的算法必須進(jìn)行可靠性測(cè)試和驗(yàn)證。

SDR3：RMU應(yīng)對(duì)接收到的臨時(shí)限速信息進(jìn)行有效性檢驗(yàn)。

SDR4：RMU在收到臨時(shí)限速后應(yīng)在規(guī)定的時(shí)間內(nèi)作出回復(fù)。

SDR5：RMU應(yīng)在規(guī)定的時(shí)間內(nèi)將臨時(shí)限速信息下發(fā)給VCM。

SDR6：若RMU在規(guī)定的時(shí)間內(nèi)沒(méi)有收到VCM的反饋，則重發(fā)TSR。

SDR7：若RMU超過(guò)規(guī)定時(shí)間未收到來(lái)自VCM的反饋，則報(bào)警。

4 基于UPPAAL的SDR驗(yàn)證

建立臨時(shí)限速下發(fā)場(chǎng)景中中各個(gè)組件的時(shí)間自動(dòng)機(jī)模型，包含調(diào)度員、DCD、RMU和VCM。由于篇幅有限，這里僅給出臨時(shí)限速下發(fā)場(chǎng)景的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型以及資源管理單元RMU的時(shí)間自動(dòng)機(jī)模型，如圖7和圖8所示。

圖7 TSR發(fā)送場(chǎng)景的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型Figure 7 The timed automata model of TSR sending scenarios

圖8 RMU的時(shí)間自動(dòng)機(jī)模型Figure 8 The timed automata model of TSR sending scenarios

把以上分析得到的SDR翻譯成BNF驗(yàn)證語(yǔ)句，在UAAPPL驗(yàn)證器中對(duì)BNF語(yǔ)句進(jìn)行驗(yàn)證，表2為部分關(guān)鍵的BNF語(yǔ)句以及驗(yàn)證結(jié)果。

表2 BNF驗(yàn)證語(yǔ)句Table 2 BNF Statement

驗(yàn)證表明，臨時(shí)限速下發(fā)場(chǎng)景滿(mǎn)足STPA模型分析得到的安全性設(shè)計(jì)需求。

5 結(jié)論

使用系統(tǒng)理論過(guò)程分析方法對(duì)基于車(chē)車(chē)通信的列控系統(tǒng)中的臨時(shí)限速下發(fā)場(chǎng)景進(jìn)行了安全性分析，得到該場(chǎng)景下的控制缺陷，通過(guò)分析控制缺陷制定了安全性設(shè)計(jì)需求。將STPA安全分析方法與UPPAAL驗(yàn)證方法相結(jié)合，在UPPAAL中驗(yàn)證了SDR的合理性。分析結(jié)果表明，STPA和UPPAAL兩種方法結(jié)合可以有效分析基于車(chē)車(chē)通信的列控系統(tǒng)的安全性。