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

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

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

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

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

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

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

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