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

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

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

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

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