列車安全距離控制形式化建模與驗(yàn)證.pdf

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

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

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

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