基于時(shí)間自動(dòng)機(jī)的CTCs-3級(jí)列控系統(tǒng)建模方法與驗(yàn)證研究.pdf

1、CTCS-3級(jí)列控系統(tǒng)的實(shí)時(shí)性依據(jù)技術(shù)規(guī)范而實(shí)現(xiàn)。如果技術(shù)規(guī)范存在缺陷，則會(huì)嚴(yán)重危及行車安全或影響行車效率。因此，有必要對(duì)列控系統(tǒng)的實(shí)時(shí)性進(jìn)行分析研究，以驗(yàn)證技術(shù)規(guī)范的正確性。
　　目前，驗(yàn)證系統(tǒng)實(shí)時(shí)性的途徑有仿真、測試、形式化方法三種。仿真和測試存在固有的缺陷，形式化方法可以最大限度地分析驗(yàn)證系統(tǒng)。通過比較多種驗(yàn)證系統(tǒng)實(shí)時(shí)性的形式化方法得出:時(shí)間自動(dòng)機(jī)理論更為適合驗(yàn)證CTCS-3級(jí)列控系統(tǒng)的實(shí)時(shí)性。
　　本文提出一種基于時(shí)

2、間自動(dòng)機(jī)的列控系統(tǒng)建模與驗(yàn)證方法?？茖W(xué)地闡述時(shí)間自動(dòng)機(jī)模型與列控系統(tǒng)的一致性、所建模型的正確性、模型驗(yàn)證結(jié)果的可信性等問題，創(chuàng)造性地提出對(duì)列控系統(tǒng)進(jìn)行VV&A分析的原則和過程，建立了基于時(shí)間自動(dòng)機(jī)的列控系統(tǒng)建模與驗(yàn)證框架，并說明了該建模與驗(yàn)證方法對(duì)CTCS-3級(jí)列控系統(tǒng)各個(gè)運(yùn)營場景的普遍通用性。其建模與驗(yàn)證的一般流程為:用時(shí)間自動(dòng)機(jī)語言規(guī)約列控系統(tǒng)的行為和動(dòng)作，得出列控系統(tǒng)的時(shí)間自動(dòng)機(jī)模型，然后用UPPAAL驗(yàn)證工具對(duì)系統(tǒng)模型所反映的特

3、性進(jìn)行驗(yàn)證。
　　以CTCS-3級(jí)列控系統(tǒng)臨時(shí)限速和等級(jí)轉(zhuǎn)換運(yùn)營場景為例，說明了該建模與驗(yàn)證方法的有效性。利用時(shí)間自動(dòng)機(jī)理論，分別建立臨時(shí)限速工作流程、等級(jí)轉(zhuǎn)換過程的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。同時(shí)，應(yīng)用UPPAAL驗(yàn)證工具對(duì)臨時(shí)限速系統(tǒng)、等級(jí)轉(zhuǎn)換過程的安全性和受限活性進(jìn)行仿真分析。找到了臨時(shí)限速技術(shù)規(guī)范中不能達(dá)到實(shí)時(shí)性要求的時(shí)間參數(shù)設(shè)置，并給出了修正值。此外，等級(jí)轉(zhuǎn)換模型成功驗(yàn)證了等級(jí)轉(zhuǎn)換過程的安全性。驗(yàn)證結(jié)果表明:該建模與驗(yàn)證方法可有