軌道交通列車運行控制系統(tǒng)的形式化建模和模型檢驗方法研究.pdf

1、在現(xiàn)代公共交通體系中，軌道交通系統(tǒng)具有不可替代的突出地位。目前，我國的軌道交通正處在一個史無前例的大發(fā)展時期，人們對它有著很高的期望和要求。如何實現(xiàn)列車安全、快速、高效地運行，是擺在相關科研人員面前的一個突出問題。列車運行控制系統(tǒng)作為軌道交通系統(tǒng)的神經(jīng)中樞，擔當著保障行車安全和提高列車運行效率的重任。隨著計算機技術在列車運行控制系統(tǒng)中的應用，安全問題顯得越發(fā)的重要和復雜，傳統(tǒng)的安全系統(tǒng)設計、分析和測試方法難以滿足以計算機技術為基礎的安全

2、系統(tǒng)的需要。近年來，基于離散數(shù)學和形式邏輯理論的形式化方法發(fā)展迅速，為解決安全計算機系統(tǒng)設計開發(fā)的正確性問題提供了一條可能的途徑。 論文針對軌道交通列車運行控制系統(tǒng)的特點，研究安全系統(tǒng)設計的理論和方法，嘗試采用形式化方法進行系統(tǒng)安全設計和驗證。論文主要以列車運行控制系統(tǒng)為研究對象，選擇自動機模型和模型檢驗方法分別作為系統(tǒng)形式化建模和驗證的方法，提出時間自動機網(wǎng)絡模型和相應的模型檢驗算法，進而給出形式化設計驗證方法ForTAN(F

3、ormalDesignandVerificationMethodsbasedonTimedAutomataNetwork)，最后以大連快軌3號線ATP車載設備為對象進行相關設計和驗證，取得了不錯的效果。這些成果這對于提高國內(nèi)軌道交通列車運行控制系統(tǒng)的安全性設計水平，掌握系統(tǒng)關鍵技術，推動列車運行控制系統(tǒng)國產(chǎn)化具有重要的理論價值和實踐意義。 論文主要的創(chuàng)新點有以下幾個方面： (1)針對軌道交通列車運行控制系統(tǒng)的特點，在有限

4、自動機模型的基礎上提出時間自動機網(wǎng)絡模型，并且給出模型的形式化定義和相關特性，提出時間自動機網(wǎng)絡模型的形式化描述語言TAN語言。和經(jīng)典自動機模型相比，時間自動機網(wǎng)絡模型有以下優(yōu)點：①通過時間自動機網(wǎng)絡模型，部分解決了經(jīng)典自動機狀態(tài)復雜性問題，使得建模過程變得較為簡便，有助于進行系統(tǒng)的形式化設計和驗證；②通過在組件自動機內(nèi)部和組件自動機之間加入時間約束集，可以對系統(tǒng)的實時性進行描述；③通過描述組件自動機之間的動作集，可以描述系統(tǒng)的并發(fā)行為

5、；④通過連續(xù)變量區(qū)域化方法有效的壓縮了系統(tǒng)的狀態(tài)數(shù)，解決了經(jīng)典自動機理論不能描述連續(xù)變量的缺陷。 (2)提出時間自動機網(wǎng)絡模型的模型檢驗方法和步驟，主要的創(chuàng)新之處在于： ①提出組件自動機(一種時間自動機)轉(zhuǎn)換為帶有時鐘狀態(tài)的有限自動機進行模型檢驗的思想；②基于DBM數(shù)據(jù)結(jié)構(gòu)，提出計算時鐘狀態(tài)和狀態(tài)遷移時間約束的算法；③提出TCTL公式在Kripke結(jié)構(gòu)上進行模型檢驗的算法，可以對系統(tǒng)安全性、無死鎖性和系統(tǒng)響應實時性進行驗

6、證。 (3)提出形式化設計驗證方法ForTAN(FormalDesignandVerificationMethodsbasedonTimedAutomataNetwork)：在需求捕捉階段采用時間自動機網(wǎng)絡模型描述系統(tǒng)需求；在系統(tǒng)設計階段，采用模型檢驗方法證明設計和需求的一致性，并保證系統(tǒng)設計滿足系統(tǒng)的安全性要求；在系統(tǒng)開發(fā)階段，從系統(tǒng)需求的形式化模型開始逐步求精，得到層次化、模塊化的系統(tǒng)實現(xiàn)框架?；跁r間自動機網(wǎng)絡的形式化設計

7、驗證方法ForTAN有以下特點：①通過設計時間自動機網(wǎng)絡中組件自動機之間的時間約束來滿足系統(tǒng)實時性的要求，采用UML順序圖和模型驗證方法可以描述和驗證系統(tǒng)的時間特性；②通過采用B方法作為形式化開發(fā)的方法，對于系統(tǒng)的時間自動機網(wǎng)絡模型進行不斷精化，反復迭代，可以獲得進行系統(tǒng)開發(fā)的偽代碼，保證系統(tǒng)開發(fā)和規(guī)范的一致性。 論文最后以大連快軌3號線ATP車載設備為應用對象，采用ForTAN方法完成了ATP車載設備控制系統(tǒng)的設計，采用時間自