基于時(shí)間自動機(jī)的CTCS-3級列控車載設(shè)備建模與驗(yàn)證.pdf

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

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

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