列控系統(tǒng)TSRS形式化建模分析與驗證.pdf

1、臨時限速是指除線路規(guī)定的限速以外，由于施工、維修等原因引起的有計劃的限速和由于自然災害、設備故障等原因引起的突發(fā)限速。臨時限速的設置關乎到提高運輸效率和保障行車安全，隨著列車速度的越來越快，對臨時限速設置的安全性要求也越來越高。臨時限速系統(tǒng)是列控系統(tǒng)的重要組成部分，是涉及到行車安全和運輸效率的安全苛求系統(tǒng)。臨時限速的工作流程具有嚴格的時序邏輯關系，體現(xiàn)出精確的時間約束特性。
　　針對臨時限速系統(tǒng)的這些特性，有必要對其工作流程的實時

2、性進行分析，采用形式化方法對系統(tǒng)的特性和行為進行建模描述，驗證所產(chǎn)生的結(jié)果在邏輯和時間上的正確性及系統(tǒng)的實時性，從而發(fā)現(xiàn)系統(tǒng)規(guī)范的不完備性和模糊性，保證系統(tǒng)的安全性，為完善設計和開發(fā)提供重要的依據(jù)。
　　本文通過分析臨時限速系統(tǒng)的結(jié)構，理清各設備之間的信息交互關系，結(jié)合臨時限速系統(tǒng)的功能及調(diào)度命令的操作流程，說明各信息的交互方式;利用時間自動機理論對臨時限速系統(tǒng)進行建模，并結(jié)合高鐵CTC調(diào)度臺分界口、CTCS等級轉(zhuǎn)換區(qū)這兩個特殊場