基于時間自動機的高鐵列控系統(tǒng)TSRS的建模分析與驗證.pdf

1、臨時限速系統(tǒng)是高鐵列控系統(tǒng)的核心構(gòu)成之一，臨時限速系統(tǒng)的工作流程嚴格依照客運專線列控系統(tǒng)臨時限速技術(shù)規(guī)范來實現(xiàn)。技術(shù)規(guī)范中規(guī)定臨時限速分為計劃性限速和突發(fā)性限速，其兩者都具有嚴格的時間邏輯關(guān)系和時間約束特性。技術(shù)規(guī)范的制定和執(zhí)行都存在一定的人為因素干擾，為了保證鐵路系統(tǒng)運營的安全和效率需要對技術(shù)規(guī)范進行合理的優(yōu)化管理。
　　臨時限速系統(tǒng)作為高鐵列控系統(tǒng)安全保障的核心環(huán)節(jié)，其安全性和受限活性受到運營場景的限制。因此運用形式化的分析方

2、法對系統(tǒng)流程、發(fā)生事件和邏輯時間關(guān)系進行形式化分析和建模描述，驗證系統(tǒng)在邏輯上的安全性和時間變化上的受限活性滿足高鐵列控系統(tǒng)的正確性要求。從而發(fā)現(xiàn)形式化描述的臨時限速系統(tǒng)存在定義上的二義性和不可達性，找出系統(tǒng)中存在的缺陷為后續(xù)臨時限速系統(tǒng)的優(yōu)化和深層次的開發(fā)提供重要的理論驗證依據(jù)。
　　本文通過分析臨時限速命令擬定校驗、下達和執(zhí)行反饋等基本操作流程，同時結(jié)合信息之間的交互關(guān)系和交互方式，并利用時間自動機理論可以建立三部分的時間自動

3、機網(wǎng)絡(luò)模型:非跨界臨時限速時間自動機模型、跨界臨時限速時間自動機模型和TSRS(Temporary Speed Restriction Server，臨時限速服務(wù)器)切換與RBC(Radio BlockCenter，無線閉塞中心)切換重疊區(qū)域臨時限速交互流程的時間自動機模型。這三個不同特殊場景下的時間自動機網(wǎng)絡(luò)模型描述了系統(tǒng)臨時限速命令的交互流程，根據(jù)系統(tǒng)要求的實時性和可達性設(shè)置不同的時間參數(shù)。根據(jù)上述時間自動機模型的規(guī)范描述和技術(shù)規(guī)范