基于時間自動機的CTCS-3級列控車載設備建模與驗證.pdf

1、鐵路系統(tǒng)歷來對安全性要求較高,CTCS-3級列控設備作為高速列車的控制系統(tǒng)對安全性的要求更高。車載設備系統(tǒng)是中國鐵路CTCS-3級列控系統(tǒng)中的重要組成部分,UPPAAL是一種基于時間自動機理論的實時系統(tǒng)分析建模驗證工具,使用UPPAAL對CTCS-3級列控系統(tǒng)車載設備中的車載安全計算機VC、司機-車載設備接口DMI和無線閉塞中心RBC進行分析建模驗證,可以驗證車載設備系統(tǒng)的特性。研究車載設備系統(tǒng)的建模,對于完善車載設備仿真系統(tǒng)性能、加快

2、車載設備系統(tǒng)軟件設計、節(jié)省現(xiàn)場測試成本等具有重要的現(xiàn)實意義。
　　 論文完成的主要工作如下:
　　 1.概述了國內(nèi)外基于形式化方法和時間自動機理論的列控系統(tǒng)建模的研究現(xiàn)狀,提出了用時間自動機對車載設備建模的意義。
　　 2.介紹了CTCS-3級列控車載設備結構、功能以及工作模式。
　　 3.分析了工作在CTCS-3級時的車載任務啟動流程、車載越行流程、列車冒進后防護流程、司機觸發(fā)的SH流程和車載任務結束流

3、程,建立了各個工作流程的狀態(tài)轉換圖,說明了車載設備的信息交互及狀態(tài)轉換過程。
　　 4.介紹了時間自動機理論及其模型檢驗工具UPPAAL的使用方法。
　　 5.基于時間自動機理論對VC、DMI和RBC分別建模:根據(jù)研究對象的特點,在合理的抽象和假設之后,確定了各個模型的狀態(tài),狀態(tài)轉換路徑、狀態(tài)轉換的約束條件和觸發(fā)事件,得到了車載設備的各個時間自動機模型。
　　 6.通過使用UPPAAL對車載設備系統(tǒng)的時間自動機模