高速磁浮運(yùn)控系統(tǒng)運(yùn)行場景的RSL建模與驗(yàn)證.pdf

1、與輪軌交通技術(shù)相比，高速磁浮交通技術(shù)更加節(jié)能和環(huán)保，并且速度也更有優(yōu)勢(shì)，是21世紀(jì)非常有競爭力的運(yùn)輸系統(tǒng)。隨著高速磁浮交通技術(shù)的日益成熟及上海磁浮列車的示范運(yùn)營，磁浮長大干線應(yīng)用是運(yùn)輸系統(tǒng)的新趨勢(shì)。如果我國能率先開展長大干線磁浮項(xiàng)目，這將成為全世界的首例。為了更好地發(fā)展長大干線磁浮交通技術(shù)，本文對(duì)磁浮交通長大干線應(yīng)用中必然產(chǎn)生的磁浮列車追蹤安全問題進(jìn)行研究。
　　首先，本文通過一個(gè)簡單RSL規(guī)約介紹了RAISE語言的一些基本概念，

2、為了更充分地掌握RAISE語言的數(shù)學(xué)特性，本文還總結(jié)了RAISE語言中的固有類型、集合、表、函數(shù)、映射及其特殊操作符。同時(shí)對(duì)如何使用RSL進(jìn)行系統(tǒng)建模與驗(yàn)證做出了闡述，并且介紹了RSL開發(fā)工具和RAISE的推理規(guī)則。
　　其次，本文通過對(duì)高速磁浮運(yùn)控系統(tǒng)的結(jié)構(gòu)和功能的研究，發(fā)現(xiàn)為了將高速磁浮技術(shù)長大干線化，還需要對(duì)其功能進(jìn)行增加，以提高系統(tǒng)的安全，因此本文增加了分區(qū)預(yù)約防護(hù)功能。結(jié)合高速磁浮交通的運(yùn)行特點(diǎn)，總結(jié)出高速磁浮系統(tǒng)的多分

3、區(qū)追蹤場景，對(duì)磁浮列車在多分區(qū)追蹤場景中的運(yùn)行過程進(jìn)行了描述。
　　然后，本文對(duì)多分區(qū)追蹤場景的安全需求進(jìn)行了分析，為了簡化模型，本文先對(duì)多分區(qū)追蹤場景進(jìn)行相應(yīng)假設(shè)，并采用RAISE語言及模塊化設(shè)計(jì)方法對(duì)長大干線高速磁浮系統(tǒng)的多分區(qū)追蹤場景進(jìn)行RSL建模，同時(shí)使用RAISE語言描述系統(tǒng)的安全需求。最后采用RSL驗(yàn)證方法對(duì)多分區(qū)追蹤場景的安全特性進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果表明在長大干線高速磁浮系統(tǒng)的多分區(qū)追蹤場景中，改進(jìn)后的高速磁浮運(yùn)控系統(tǒng)