基于安全狀態(tài)機的RBC系統(tǒng)行車許可模塊的建模與驗證.pdf

1、中國鐵路進入了跨越式大發(fā)展時期，當(dāng)前正在研究的是基于GSM-R無線通信系統(tǒng)的車-地雙向信息傳輸?shù)腃TCS-3級列控系統(tǒng)，它可以極大的提高鐵路運輸?shù)陌踩?、可靠性以及運輸效率。無線閉塞中心RBC（Radio Block Center）是CTCS-3級列控系統(tǒng)的地面核心設(shè)備，它通過計算并向列車發(fā)送運行許可來完成安全控車。因此，設(shè)計合理的行車許可的算法尤為重要。 本文研究的主要內(nèi)容是MA（Movement Authority）的算法原

2、理、功能需求和實現(xiàn)，對MA進行模塊劃分，基于安全狀態(tài)機理論對MA進行建模與分析，并且利用實時系統(tǒng)檢驗工具UPPAAL仿真并模擬安全狀態(tài)機模型，最后對模型進行檢驗，說明MA算法的正確性。以下是論文完成的主要工作： 一、首先從RBC的功能與接口入手，對MA的基本含義，功能需求以及算法原理進行了詳細的分析和闡述?；贛A的功能需求，對其進行功能模塊的劃分，包括完全監(jiān)控模式下的MA計算，引導(dǎo)模式下的MA計算，等級轉(zhuǎn)換場景中的MA計算，相

3、鄰RBC交接的混合MA計算，包含臨時限速信息的MA計算以及MA的管理功能，并且對各個功能模塊的實現(xiàn)做出分析和設(shè)計； 二、然后基于MA算法的原理，對MA進行結(jié)構(gòu)化的模塊劃分，分為五個模塊，即串路徑模塊，列車定位模塊，更新路徑模塊，MA計算模塊，MA發(fā)送模塊。論文針對這五個模塊，采用安全狀態(tài)機理論對其進行建模和研究，運用安全狀態(tài)機分層結(jié)構(gòu)，并發(fā)控制，優(yōu)先級控制這三個重要特征，結(jié)合狀態(tài)抽象及轉(zhuǎn)移條件控制，實現(xiàn)各模塊的邏輯功能以及在特定

4、場景下的MA計算方法； 三、最后論證了UPPAAL模擬安全狀態(tài)機模型的合理性，并且基于UPPAAL對MA進行建模和模型檢驗，為MA應(yīng)用軟件設(shè)計提供了理論依據(jù)。 論文的創(chuàng)新點在于提出行車許可的算法，探索利用安全狀態(tài)機理論，為RBC系統(tǒng)的行車許可模塊進行建模與分析，提出行車許可的設(shè)計方案，并且用基于時間自動機的模型檢驗工具UPPAAL對安全狀態(tài)機模型進行驗證。安全狀態(tài)機模型界面友好，可操作性強，進而可以展望推廣到利用安全狀態(tài)