車車通信列控系統資源管理單元安全性分析

劉振宇，李 晶

（北京城建設計發展集團股份有限公司，北京 100045）

隨著軌道交通行業的快速發展，傳統列控系統暴露出一系列弊端，例如客運壓力大、行車效率低、軌旁設備繁多等[1]。眾多科研機構和企業積極進行新一代列控系統的開發，對列控系統的結構與功能進行進一步優化。

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

本文重點對基于車車通信列控系統的 RMU(resource management unit，資源管理單元)進行安全性分析。以RMU發送TSR (temporary speed restriction，臨時限速)場景為例，構建了列控系統的分層控制結構。根據列控系統的控制結構，判斷該過程中危險控制行為并找到控制缺陷。利用控制缺陷得到相關SDR(security design requirements，安全性設計需求)。通過UPPAAL工具搭建TSR發送場景下的時間自動機網絡模型，最后把SDR翻譯為UPPAAL可識別的語言，以此來驗證SDR的合理性。

1 基于車車通信的下一代列控系統介紹

基于車車通信的列控系統的系統結構可以分為 3層，分別為：運營控制層、車載控制層以及軌旁控制層，如圖1所示。運營控制層主要由DCD (dynamic capacity decision，動態運能決策系統)和RMU構成。動態運能決策系統的功能是發送行車計劃和調度命令。RMU主要負責在線列車管理與臨時限速下發。車載控制層是整個列控系統的核心，主要由VCM (vital computer management，車載列車管理)和 VCI (vital computer interlocking，車載聯鎖)組成，具有完成移動授權計算、列車超速防護和進路排列等功能；軌旁控制層主要由OC (object controller，對象控制單元)等設備組成，具有信號機、轉轍機等軌旁設備的控制和表示功能。

圖1 基于車車通信列控系統的系統結構Figure 1 Structure of train control system based on vehicle-vehicle communications

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

圖2 RMU對外設備交互圖Figure 2 Diagram of external device interaction

2 研究方法介紹

2.1 STPA模型概述

STAMP模型是基于系統理論的事故分析模型，它重點關注系統組件間的交互及控制機制[5]。STAMP理論采用多層次的系統結構來表征系統內部單元之間的信息流，主要是控制命令和反饋結果的。系統安全的重點由防止組件失效轉換為實施行為的安全約束，將安全問題轉換為控制問題而不是可靠性問題[6]。STAMP已經成功應用于多種安全苛求系統的分析，涉及航空航天、國防工業、交通運輸、化學工業和醫藥生成等多個領域[7]。

STPA基于STAMP理論構建的系統控制圖進行分析，從外部輸入開始針對控制回路的每一個環節進行分析，辨識致因因素。STPA以系統級危險作為輸入，主要通過以下4個步驟辨識導致危險出現的根本原因[8]：

第1步：針對系統級危險，確立安全約束；

第2步：搭建多層次的系統結構。搭建多層次的系統結構，可以研究系統內部各層次信息流動的過程，從交互過程中尋找系統中存在的不安全因素。

第3步：尋找導致系統危險的原因。針對所建立的分層控制結構圖中的控制行為，辨識以下不安全控制行為：①系統發出的未定義安全要求的控制或不符合安全約束控制；②提供不安全的控制從而導致危險；③控制行為本身是安全的但時序不正確；④系統進行控制的時間不合要求。

第4步：分辨控制缺陷。該步驟需要對系統的各個控制閉環中的各單元進行研究，從而分辨出系統的控制缺陷，如圖3所示。

圖3 控制缺陷分類Figure 3 Classification of unsafe factors

2.2 UPPAAL 和時間自動機

時間自動機是在有限自動機的基礎上添加了時間約束產生的[9]，可以有效地對實時系統進行建模和驗證[10]，基于車車通信的列控系統是實時系統。

UPPAAL是一個對實時系統建模和驗證的工具[11]，為實時系統的模型驗證提供了一種規范化的驗證語法-BNF(Backus-Naur Form，巴科斯范式)語法[12]，其規則如下：

3 TSR下發場景的安全性分析

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

3.1 TSR下發場景介紹

臨時限速命令具有為列車提供安全防護和運行調整的功能。TSR下發的第一步人工輸入 TSR參數，DCD接收到參數后生成臨時限速命令，經過相關協議拆分和轉換后發送給相關RMU進行有效性驗證。TSR檢驗無誤后進行保存并等待執行，如果有效性驗證失敗，通過提示，值班員可在調整TSR參數后再次發送命令。RMU驗證成功后，將TSR命令發送給管轄范圍內的列車，VCM接收到TSR后，執行臨時限速命令，然后向RMU發送反饋信息。

3.2 基于STPA的TSR下發場景安全分析

3.2.1 定義系統級危險及安全約束

由相關標準和規范可以得到列控系統的系統級危險：列車速度大于安全速度或者超出安全距離限制，標記為“H1”作為要分析的系統級危險，針對該系統級危險，安全條件是列車運行控制系統必須保證列車運行速度不超過安全速度或超出安全距離限制。

3.2.2 建立待分析系統的分層控制結構

使用分層框圖對基于車車通信列控系統的分層控制結構進行描述。分層控制結構不僅包括列控子系統(例如 RMU，DCD 等)，也包括調度員以及司機等。圖4為RMU向VCM發送臨時限速命令的分層控制結構圖，圖中實線框內為基于車車通信的列控系統內部包含的單元，虛線框內為列控系統外部單元。

圖4 分層控制結構Figure 4 Hierarchical control structure

在構建分層控制結構圖之后，可以細化系統的交互過程，得到過程模型，如圖5所示。過程模型是控制器對被控過程的理解和認知[13]，控制器中的相關算法也是在此基礎上形成的。

圖5 過程模型Figure 5 Process model

3.2.3 不安全控制行為辨識

根據基于車車通信的列控系統在臨時限速下發場景中的控制行為，針對危險H1，辨識出可能的不安全控制行為，表1為部分不安全控制行為。

表1 不安全控制行為Table 1 Unsafe control behavior

3.2.4 控制缺陷分析

最后需要研究列控系統的控制缺陷，找到不安全控制場景出現的因素。TSR下發場景中的不安全因素如圖6所示。

圖6 TSR下發場景中的不安全因素Figure 6 Unsafe factors in TSR sending scenarios

控制缺陷如下：

CD1：調度員疏忽，忘記下達臨時限速命令。

CD2：調度員疏忽，過晚的下達臨時限速命令。

CD3：調度員操作不當，下達錯誤的臨時限速命令。

CD4：DCD未接受到調度員操作命令，或收到錯誤的命令，過晚收到命令。

CD5：DCD自身硬件出現故障。

CD6：DCD的算法設計存在缺陷。

CD7：DCD未向RMU下達臨時限速。

CD8：DCD對TSR的解析出現錯誤。

CD9：DCD過晚地向RMU下達臨時限速信息。

CD10：RMU未收到來自DCD的TSR，或收到錯誤的TSR，超時收到TSR。

CD11：RMU自身硬件出現故障。

CD12：RMU的算法設計存在缺陷。

CD13：RMU未向VCM下達臨時限速。

CD14：RMU解析TSR出現錯誤。

CD15：RMU過晚地向VCM下達臨時限速信息

CD16：VCM未收到來自RMU的TSR，或收到錯誤的TSR，超時收到TSR。

CD17：VCM對TSR解析錯誤。

CD18：VCM自身硬件出現故障。

CD19：VCM的算法設計存在缺陷。

CD20：速度傳感器速度測量誤差過大。

3.2.5 安全性設計需求

對所得的控制缺陷進行分析，制定出相應的安全性設計需求，為UPPAAL模型驗證語句提供來源。部分與RMU相關的安全性設計需求如下：

SDR1：RMU必須進行冗余和可靠性設計。

SDR2：RMU系統的算法必須進行可靠性測試和驗證。

SDR3：RMU應對接收到的臨時限速信息進行有效性檢驗。

SDR4：RMU在收到臨時限速后應在規定的時間內作出回復。

SDR5：RMU應在規定的時間內將臨時限速信息下發給VCM。

SDR6：若RMU在規定的時間內沒有收到VCM的反饋，則重發TSR。

SDR7：若RMU超過規定時間未收到來自VCM的反饋，則報警。

4 基于UPPAAL的SDR驗證

建立臨時限速下發場景中中各個組件的時間自動機模型，包含調度員、DCD、RMU和VCM。由于篇幅有限，這里僅給出臨時限速下發場景的時間自動機網絡模型以及資源管理單元RMU的時間自動機模型，如圖7和圖8所示。

圖7 TSR發送場景的時間自動機網絡模型Figure 7 The timed automata model of TSR sending scenarios

圖8 RMU的時間自動機模型Figure 8 The timed automata model of TSR sending scenarios

把以上分析得到的SDR翻譯成BNF驗證語句，在UAAPPL驗證器中對BNF語句進行驗證，表2為部分關鍵的BNF語句以及驗證結果。

表2 BNF驗證語句Table 2 BNF Statement

驗證表明，臨時限速下發場景滿足STPA模型分析得到的安全性設計需求。

5 結論

使用系統理論過程分析方法對基于車車通信的列控系統中的臨時限速下發場景進行了安全性分析，得到該場景下的控制缺陷，通過分析控制缺陷制定了安全性設計需求。將STPA安全分析方法與UPPAAL驗證方法相結合，在UPPAAL中驗證了SDR的合理性。分析結果表明，STPA和UPPAAL兩種方法結合可以有效分析基于車車通信的列控系統的安全性。