基于SCADE的測速定位系統(tǒng)模型設(shè)計

劉 歡，李 耀

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

基于SCADE的測速定位系統(tǒng)模型設(shè)計

劉 歡，李 耀

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

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

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

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

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

1 SCADE簡介

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

圖1 SCADE嵌入式軟件模型設(shè)計圖

1.1 需求建模

SCADE Suite以嚴(yán)格的數(shù)學(xué)模型作為基礎(chǔ)，所建模型具有嚴(yán)格的數(shù)學(xué)語義，模型具有精確性、完整性、一致性、可驗證性及無二義性[3]。SCADE擁有數(shù)據(jù)流圖和安全狀態(tài)機(jī)兩套建模機(jī)制，分別適合于連續(xù)系統(tǒng)和離散系統(tǒng)建模。兩套機(jī)制通過SCADE融合，能對各種混合系統(tǒng)進(jìn)行安全性建模。

1.2 模型驗證

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

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

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

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

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

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

圖2 SCADE形式化驗證流程圖

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

2 測速定位

列車的測速定位是ATP系統(tǒng)的重要功能。精確的速度和位置參數(shù)，是列車實現(xiàn)超速防護(hù)、保證列車安全運行的前提。國內(nèi)外對列車測速定位方法的研究中，諸多專家學(xué)者和研究人員提出了各具特色的方法。表1對常用的列車定位方法及其優(yōu)缺點進(jìn)行了總結(jié)[5]。

表1 列車定位方法總結(jié)

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

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

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

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

2.2 多普勒雷達(dá)測速定位

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

2.3 查詢應(yīng)答器定位

有源、無源應(yīng)答器安裝在鐵路線路上的固定地點，其存儲了當(dāng)前位置坐標(biāo)信息與整條線路的數(shù)據(jù)信息，查詢應(yīng)答器通過列車上的查詢器與線路上的應(yīng)答器之間的數(shù)據(jù)交互，實現(xiàn)列車的定位功能。

3 SCADE的測速定位模型設(shè)計

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

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

圖3 測速定位原理框圖

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

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

在求得d后，根據(jù)列車在周期內(nèi)的脈沖數(shù)就可獲得列車的運行速度。

式（2）中：CYCLE—單位時間，N—單位時間內(nèi)測得的脈沖數(shù)。

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

圖4 脈沖速度測量SCADE模型

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

3.2 多普勒雷達(dá)測速定位模型

當(dāng)雷達(dá)傳感器與速度傳感器速度判斷后，列車處于空轉(zhuǎn)或滑行狀態(tài)時，需要使用雷達(dá)傳感器的速度信息進(jìn)行速度補償。在單位時間CYCLE內(nèi)，可認(rèn)為雷達(dá)傳感器速度信息即為列車速度。

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

圖5 雷達(dá)與速度傳感器速度比較模型

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

3.3 應(yīng)答器校正模型

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

圖6 應(yīng)答器校正模型

當(dāng)應(yīng)答器信號Balise_Action為真，列車位置進(jìn)行絕對校正，列車位置信息即為所接收應(yīng)答器位置信息Balise_LocationInfo，位置誤差修正為0。

3.4 車輪輪徑校正模型

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

式（3）中：L—校正應(yīng)答器的間距；n—正常車輪旋轉(zhuǎn)一周的脈沖數(shù)；N—校正路段內(nèi)，車輪的脈沖數(shù)。

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

圖7 車輪校正模型

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

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

4 模型驗證

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

圖9 安全屬性模型

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

圖10 模型驗證結(jié)果

5 結(jié)束語

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

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

[2]張 路.基于SCADE的CBTC區(qū)域控制器軟件開發(fā)[D].北京：北京交通大學(xué)，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區(qū)域控制器軟件測試方法研究 [D].北京：北京交通大學(xué)，2010.

[5]崔 超,張亞東,郭 進(jìn).改進(jìn)的灰度預(yù)測在列車輪徑校正中的研究 [J].鐵道標(biāo)準(zhǔn)設(shè)計，2016（1）：139-143.

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

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

[8]張 源，張洪宇.現(xiàn)代鐵路列車跟蹤與定位技術(shù)的研究[J].鐵路計算機(jī)應(yīng)用，2011，20（4）.

責(zé)任編輯 徐侃春

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

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