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

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

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

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