CTCS-3級列控系統(tǒng)RBC行車許可生成的形式化建模與分析.pdf

1、CTCS-3級列控系統(tǒng)是我國在引進國外新技術并不斷消化吸收再創(chuàng)新的情況下,研發(fā)出的適合本國國情的列控系統(tǒng)。目前我國鐵路正大力應用和研究該系統(tǒng),它極大地提高了鐵路運輸?shù)目煽啃浴踩?。但是根?jù)我國鐵路的基本國情,列控系統(tǒng)仍然需要不斷完善與研究,而需求規(guī)范是系統(tǒng)開發(fā)的起點與基礎,必須對列控系統(tǒng)規(guī)范進行嚴格的分析驗證,消除規(guī)范的歧義性才能使列控系統(tǒng)朝著更安全更可靠的方向發(fā)展。
　　 行車許可生成管理是RBC的主要功能之一,RBC根據(jù)不

2、同的運營場景計算不同的行車許可并發(fā)送給列車,列車按照行車許可命令安全控車。因此根據(jù)需求規(guī)范分析行車許可的生成對列控系統(tǒng)的安全高效運行具有重要意義。
　　 本文針對上述問題,首先,基于行車許可不同的功能需求設計不同的應用層模塊;其次,研究不同運營場景下的行車許可生成過程;最后,根據(jù)CTCS-3級列控系統(tǒng)行車許可的生成機制,設計了一種基于著色Petri網理論的行車許可生成模型,運用CPN-Tools仿真工具動態(tài)仿真了CTCS-3級列

3、控系統(tǒng)不同運營場景下的行車許可生成過程,觀察列車運行過程中的通信機制及信息傳輸,并通過狀態(tài)空間分析法和性能分析法分析了模型的一些屬性及時間因素對行車許可生成的影響。
　　 仿真結果表明,所建立的模型符合設計的要求,能夠在不同的運營場景下完成相應的MA計算;通過生成的狀態(tài)空間報告圖分析驗證系統(tǒng)的一些屬性都符合列控系統(tǒng)的規(guī)范要求;最后加入參數(shù)對設計的模型進行優(yōu)化,得出系統(tǒng)最合理的延遲范圍。為行車許可模塊的設計提供一種規(guī)范的正確的軟件