列車安全距離控制形式化建模與驗證.pdf

1、我國鐵路近些年發(fā)展形勢迅猛,列車的安全行駛問題同時逐漸受到人們的高度關(guān)注。列車車載自動防護系統(tǒng)(ATP)的核心功能是對列車的行車安全進行安全防護,最大限度地保障列車的行車安全。列車車載自動防護系統(tǒng)對于列車運行控制系統(tǒng)來說十分的重要,列車任何時間的具體位置以及列車運行的行車間隔、速度、加速度等重要信息都是由列車定位的功能來實現(xiàn)?，F(xiàn)代化的列車車載自動防護系統(tǒng)采用了先進的信息技術(shù),然而其系統(tǒng)本身由于系統(tǒng)化、網(wǎng)絡(luò)化、復(fù)雜化且具有極強的實時性及其

2、分布式設(shè)備特征以及其混合屬性的特點,采用形式化方法建立其相對應(yīng)的設(shè)備系統(tǒng)模型能夠更最大程度地理解和分析列車車載自動防護系統(tǒng),并可以用更小的成本盡可能的觀察系統(tǒng)在邏輯正確性、整體一致性和功能完備性上的表現(xiàn)。
　　形式化建模仿真語言Event-B是一種處于發(fā)展前言的語言,其建模仿真平臺是由Rodin這款軟件來提供。該語言中的Machine部分經(jīng)過不斷提精之后,利用計算機模擬計算其中事件的不變式能夠達到模擬真實效果的系統(tǒng)狀態(tài)的一個行為效

3、果;該語言中的Context部分經(jīng)過不斷的擴展之后,模擬出來的環(huán)境可以更趨于真實的環(huán)境;與此同時, Event-B中應(yīng)用的完善的數(shù)學理論具備了一般形式化理論方法中所應(yīng)用的數(shù)學理論,該語言能夠把系統(tǒng)運行過程中的各種狀態(tài)通過使用數(shù)學的方法進行表述和計算,同時檢查系統(tǒng)的邏輯正確性與完備性。所以,能夠?qū)ο到y(tǒng)的形式化建模仿真起到有效的作用。
　　本文需要一套統(tǒng)一的語義理論和一致的高層構(gòu)建定理來保證模型能夠進行正確的轉(zhuǎn)化和有效的驗證,用來保證

4、產(chǎn)生的模型的正確性,并且對模型的規(guī)范、精化和驗證提供工具的支持。Event-B語言是基于嚴格數(shù)學定義的形式化方法,能夠精確、清晰地描述系統(tǒng)結(jié)構(gòu)的特性。文章采用形式化方法Event-B研究了高速列車安全距離控制形式化驗證的問題,以Event-B形式化仿真工具Rodin為基礎(chǔ),通過結(jié)合多智能體理論,引入感知模塊法則,實現(xiàn)了 RBC與列車的車地通信,建立了多列車運行的安全距離控制模型。仿真研究了高速列車最小間隔追蹤控制運行,對列車安全距離控車