基于SCADE的測速定位系統模型設計

劉 歡，李 耀

（西南交通大學 信息科學與技術學院，成都 610031）

基于SCADE的測速定位系統模型設計

劉 歡，李 耀

（西南交通大學 信息科學與技術學院，成都 610031）

針對列車測速定位系統的精度和可靠性直接影響著列車運行安全和效率的問題，提出了基于SCADE的測速定位系統模型設計，介紹SCADE需求建模以及模型驗證方法，分析了一種測速定位模型；在SCADE平臺上建立了測速定位系統的模型，通過仿真與驗證，證明模型完全滿足測速定位的系統需求與安全性。

SCADE； 測速定位； 安全軟件； 形式化驗證

列車自動控制系統（ATC，Automatic Train Control）由3個子系統組成：列車自動防護（ATP，Automatic Train Protection）、列車自動運行（ATO，Automatic Train Operation）、列車自動監控（ATS，Automatic Train Supervision）。列車測速定位系統是ATP系統的重要組成部分。列車安全行駛離不開列車測速定位系統提供的速度及位置信息。列車通過實時檢測自身位置信息以及速度信息，結合線路數據，臨時限速信息，為列車運行計算行車許可，在保證列車安全運行的前提下，提高運輸效率[1]。測速定位軟件是典型的安全苛求系統（Safety Critical System），直接關系到列車的運行安全。

傳統的軟件開發方法存在周期長、投入高、風險大、效率低、可靠性低的缺點。高安全性應用開發環境（SCADE，Safety Critical Application Development Environment）針對實時嵌入式系統，為高安全性系統和軟件開發人員提供完整的基于模型的解決方案，具有開發成本低、開發風險小、效率高的諸多優勢。本文使用SCADE對測速定位系統進行模型的建立，證明SCADE開發能夠滿足測速定位功能需求，且滿足其安全性的要求。

1 SCADE簡介

SCADE采用同步編程理論，以Lustre語言為核心，意在創建無歧義的軟件模型[2]。SCADE嵌入式軟件模型設計如下圖1所示。

圖1 SCADE嵌入式軟件模型設計圖

1.1 需求建模

SCADE Suite以嚴格的數學模型作為基礎，所建模型具有嚴格的數學語義，模型具有精確性、完整性、一致性、可驗證性及無二義性[3]。SCADE擁有數據流圖和安全狀態機兩套建模機制，分別適合于連續系統和離散系統建模。兩套機制通過SCADE融合，能對各種混合系統進行安全性建模。

1.2 模型驗證

SCADE模型本身也是一種軟件需求，其主要驗證技術包括：

（1）Reviews，對SCADE模型進行走查，保證模型本身的正確，無歧義性；

（2）Traceability analysis，SCADE模型與系統需求之間的可追蹤性分析；

（3）Check and Simulation，功能測試，驗證模型與需求的一致性，盡可能地排除模型設計中錯誤；

（4）模型覆蓋率測試（MTC,Model Test Coverage），根據覆蓋率準則，實現仿真場景在模型中的覆蓋率程度分析，仿真出模型未覆蓋路徑，找出模型設計錯誤以及需求錯誤，確保需求已經正確的實現，評估模型功能測試的完備程度，覆蓋率分析步驟包括：模型插裝（Model Instrumentation）、覆蓋率獲取（Acquisition）、覆蓋率分析（Analysis）、生成報表（Reporting）[4]；

（5）形式化驗證（Formal Verification）通過設計系統的安全性特性觀察器，用數字驗證的方式實現特性觀察器，驗證軟件需求中的安全性特征是否滿足，補充功能測試的不足，證明系統的安全性與可靠性，流程如圖2所示；

圖2 SCADE形式化驗證流程圖

（6）時間和堆棧分析，(Time and stack analysis)提前確定系統程序的最壞運行時間和堆棧使用情況是每一個嚴格的嵌入式系統開發人員必須考慮的問題。SCADE引入了時間與堆棧分析器，可以對建立好的模型進行時間堆棧分析，設計人員可以基于此對模型進行優化。

2 測速定位

列車的測速定位是ATP系統的重要功能。精確的速度和位置參數，是列車實現超速防護、保證列車安全運行的前提。國內外對列車測速定位方法的研究中，諸多專家學者和研究人員提出了各具特色的方法。表1對常用的列車定位方法及其優缺點進行了總結[5]。

表1 列車定位方法總結

城市軌道交通中，各大信號設備廠商的定位技術各不相同，如有的公司采用的定位技術是：（1）基于脈沖速度傳感器與雷達速度傳感器，同時結合應答器信息進行位置確定；（2）程編碼計；（3）基于脈沖速度傳感器與加速度傳感器，同時結合應答器信息進行位置確定。

本文提出基于脈沖速度傳感器、雷達傳感器和查詢應答器的測速定位模型，并考慮了車輪輪徑磨損對列車測速定位的影響，同時提出了空轉和打滑場景下的誤差修正算法。

2.1 輪軸脈沖速度傳感器測速定位

輪軸測速定位的基本工作原理是先測得車輪的轉速脈沖，再通過公式計算得出列車的走行速度[6]。輪軸速度傳感器因為精度高，在國內列車測速定位中廣泛被使用，將其作為基準速度信息，但是，車輪的空轉、打滑和磨損，會導致輪軸測速定位誤差的加大。

2.2 多普勒雷達測速定位

多普勒雷達測速的工作原理是通過測量發射電磁波與接收電磁波的頻移計算得出列車的速度信息[7]。它的精度主要受到列車振動、雷達傳感器自身誤差以及傳感器安裝誤差影響，但不受列車空滑狀態的影響，所以雷達傳感器通常配合其它定位方法使用。

2.3 查詢應答器定位

有源、無源應答器安裝在鐵路線路上的固定地點，其存儲了當前位置坐標信息與整條線路的數據信息，查詢應答器通過列車上的查詢器與線路上的應答器之間的數據交互，實現列車的定位功能。

3 SCADE的測速定位模型設計

根據脈沖速度傳感器、雷達傳感器和查詢應答器的工作原理，本文設計測速定位系統模型原理：列車運行過程中，ATP同時檢測速度傳感器速度信息與雷達傳感器速度信息，當速度傳感器的速度信息與雷達傳感器的速度信息差值在容許范圍（考慮測量誤差）內，速度傳感器信息作為基準速度信息；當差值超出容許范圍，車載ATP進行空滑報警，采用雷達傳感器的速度信息進行速度補償。同時，當列車經過地面應答器，通過車地信息的傳輸，實現列車位置的絕對修正。另外，考慮列車車輪的輪徑對脈沖速度傳感器速度測量的影響，設計列車輪徑校正模型，在列車運行前，對列車車輪輪徑進行校正。

本文測速定位模型原理框圖如圖3所示。

圖3 測速定位原理框圖

3.1 輪軸脈沖速度傳感器測速定位模型

速度傳感器安裝于車軸之上，為保證系統可靠性，配置主備兩套速度傳感器。隨著列車的運行，輪軸每轉動一周，脈沖速度傳感器就會輸出一定的脈沖數。在已知車輪直徑D、車輪轉動一周產生固定脈沖數n的情況下，求得列車在每個脈沖內的走行距離d，公式如下：

在求得d后，根據列車在周期內的脈沖數就可獲得列車的運行速度。

式（2）中：CYCLE—單位時間，N—單位時間內測得的脈沖數。

脈沖速度測量SCADE模型如圖4所示。

圖4 脈沖速度測量SCADE模型

圖4中，Train_WheelOnePluse為1脈沖速度傳感器的輸入信息，NORMALPLUSE_ONECYCLE為車輪旋轉一周所產生的脈沖個數，本文以上海地鐵A型車為例，NORMALPLUSE_ONECYCLE取值為104。CYCLETIME為模型采樣周期，取值0.1 s。SPEEDERRRATE為速度脈沖傳感器的采樣誤差率，根據工程數據，本文取值為0.02。模型輸出Train_WheelOne_Vel、Train_WheelOne_Dis、Train_ WheelOne_TolErr分別為由1脈沖速度傳感器數據所測列車的速度信息、當前位置以及位置誤差。2脈沖速度傳感器測量方式類似。

3.2 多普勒雷達測速定位模型

當雷達傳感器與速度傳感器速度判斷后，列車處于空轉或滑行狀態時，需要使用雷達傳感器的速度信息進行速度補償。在單位時間CYCLE內，可認為雷達傳感器速度信息即為列車速度。

雷達傳感器與速度傳感器速度比較SCADE模塊如圖5所示。

圖5 雷達與速度傳感器速度比較模型

圖5中，Train_RadarInfo為雷達速度傳感器所測列車信息，RADAR_SPEED_ERRCAPACITY為雷達誤差容許范圍。輸出SliSpi_Sig為列車空轉信號。當列車脈沖速度傳感器所測速度與雷達傳感器所測速度的差值小于雷達誤差容許范圍時，輸出列車滑行信號。

3.3 應答器校正模型

列車速度測量誤差會隨著列車運行里程的增加而不斷累積，所以，使用應答器對列車的位置進行修正十分必要。應答器的位置修正使用電磁耦合、感應。當列車經過線路上的應答器時，車載查詢器接收地面應答器的固定位置信息，實現列車位置的絕對修正。應答器校正模型如圖6所示。

圖6 應答器校正模型

當應答器信號Balise_Action為真，列車位置進行絕對校正，列車位置信息即為所接收應答器位置信息Balise_LocationInfo，位置誤差修正為0。

3.4 車輪輪徑校正模型

由速度傳感器計算列車運行位移方法可以看出，車輪的輪徑精確度影響著列車測速定位的精確度，隨著列車運行里程的增加，車輪輪徑的影響也是累積的，所以，對列車進行車輪輪徑校正是不可或缺的。校正方法如下，在固定線路位置上設置輪徑校正應答器，當列車越過第1個校正應答器時，列車保持勻速直線運行，防止空滑現象的發生，同時開始計數脈沖。當列車經過第2個校正應答器時，脈沖計數結束，輪徑校正結束。輪徑校正后直徑為：

式（3）中：L—校正應答器的間距；n—正常車輪旋轉一周的脈沖數；N—校正路段內，車輪的脈沖數。

車輪校正SCADE模型如圖7所示。

圖7 車輪校正模型

列車開始處于初始化Diaadj_Init狀態，當車輪校正開始應答器信號為真，列車進入TrainDia_Cal脈沖計數模塊，當車輪校正結束應答器信號Balise_ AdjustEnd_Sig為真，列車進入Dia_Cal輪徑計算狀態，輪徑計算模型如圖8所示。以上海地鐵A型車為例，列車車輪直徑正常范圍為770～840 mm之間，超出此范圍，應給出輪徑報廢信號Train_ WheelScrap_Sig。

圖8 車輪校正輪徑計算模型

4 模型驗證

為保證列車運行安全，模型設計完成后需要對模型進行安全驗證。本文采用形式化驗證方法，對系統進行安全驗證。IEEE1474標準中規定，在城市軌道交通中，當定位誤差大于10 m，則定義為列車丟失，列車將實施緊急制動。本文以此作為安全需求，對所設計的測速定位模型進行驗證，安全屬性模型如圖9所示，當定位模型中列車當前位置誤差CurLoc_ TolErr超過10 m時，列車必須進入失效狀態，輸出緊急制動。

圖9 安全屬性模型

利用SCADE的模型檢測工具Design Verifier驗證安全屬性，結果為Valid，表明模型滿足安全屬性，如圖10所示。

圖10 模型驗證結果

5 結束語

本文采用高安全性實時嵌入軟件SCADE對ATP的關鍵子系統，測速定位子系統進行了建模。采用基于速度傳感器、雷達傳感器和加速度傳感器相結合的測速思想，綜合考慮了列車運行過程中列車輪徑磨損、列車空轉、列車打滑狀態對測速定位的影響，采取速度修正方式，同時結合地面應答器，對列車的位置進行絕對的校正，模型提高了測速定位系統的精度，同時，采用SCADE的形式化安全驗證，證明了模型符合系統安全屬性，具備高安全性與可靠性。

[1]周鈺威.ATP車載安全計算平臺及測速定位功能的研究 [D].北京：北京交通大學，2012.

[2]張 路.基于SCADE的CBTC區域控制器軟件開發[D].北京：北京交通大學，2010.

[3]CHO C B,CHOI D H,QUAN zhong-hua,et al.Modeling of CBTC Carborne ATO functions using SCADE[C].Proc of the 11th International Conference on Control,Automation and Systems.[S.I.]:IEEE Press,2011:1089-1093.

[4]李 雷.基于SCADE的CBTC區域控制器軟件測試方法研究 [D].北京：北京交通大學，2010.

[5]崔 超,張亞東,郭 進.改進的灰度預測在列車輪徑校正中的研究 [J].鐵道標準設計，2016（1）：139-143.

[6]李 耀，陳榮武，謝 剛.基于SCADE與QNX平臺的列車測速定位安全軟件[J].計算機應用研究，2013（10）：3044-3047.

[7]王靈麗.基于CBTC的地鐵列車組合定位技術研究 [D].成都：西南交通大學，2014.

[8]張 源，張洪宇.現代鐵路列車跟蹤與定位技術的研究[J].鐵路計算機應用，2011，20（4）.

責任編輯 徐侃春

Model of Speed Measurement and Positioning System based on SCADE

LIU Huan,LI Yao
( School of Information Science &Technology,Southwest Jiaotong University,Chengdu 610031,China)

Focusing on the problem that the safety and efficiency of train operation was affected directly by the accuracy and reliability of the Speed Measurement and Positioning System,this article proposed a design method for the model of Speed Measurement and Positioning System based on SCADE,introduced the method of requirement modeling and model verification,analyzed a model of speed measurement and positioning.The model of Speed Measurement and Positioning System was established by SCADE.Simulation and verifcation proved that the safety requirement of the System was completely satisfed.

SCADE;Speed Measurement and Positioning System;safety software;formal verifcation

U284.482∶TP39

A

1005-8451（2016）07-0008-05

2016-01-04

劉 歡，在讀碩士研究生；李 耀，在讀博士研究生 。