基于UML與UPPAAL的高鐵列控臨時限速切換場景建模與驗證

打開文本圖片集

摘要：為提高高速鐵路列控臨時限速命令在臨時限速服務(wù)器（temporary speed restriction server，TSRS）與無線閉塞中心（radio block center， RBC）跨界重疊區(qū)域信息傳遞過程的時效性和安全性，建立TSRS切換與RBC切換跨界重疊區(qū)域限速流程的數(shù)學(xué)模型，根據(jù)中國列車運行控制系統(tǒng)（Chinese train control system，CTCS）CTCS-2/CTCS-3高鐵列控系統(tǒng)間臨時限速命令交互的特點，采用統(tǒng)一建模語言（unified modeling language，UML）與時間自動機模型理論相結(jié)合的方法，采用形式化驗證工具UPPAAL尋找臨時限速命令在跨界重疊區(qū)域信息傳遞的不足和漏洞。（剩余11731字）