發(fā)布時間：2017-06-02 09:24

  本文關(guān)鍵詞：列控安全計算機管理機制的形式化驗證與實現(xiàn)，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著近年來區(qū)域經(jīng)濟一體化的逐步形成,城市間人員流動的加快,基于傳統(tǒng)架構(gòu)的列車運行控制系統(tǒng)逐漸顯露出不足。為滿足人們出行快速、便捷的需求,在保證安全性和運輸效率的同時,提高對多種系統(tǒng)運行平臺的兼容性,針對下一代列控系統(tǒng)的研究已經(jīng)展開。作為實現(xiàn)數(shù)據(jù)運算處理功能的載體,列控安全計算機一直是列控系統(tǒng)研究工作的關(guān)鍵部分。管理單元作為系統(tǒng)內(nèi)部的中樞神經(jīng),主要實現(xiàn)安全計算機運行的管理機制,對運算協(xié)處理器以及安全輸入輸出單元進行調(diào)配,并對輸出結(jié)果進行表決。而其中運行管理機制的驗證與實現(xiàn),對于列控安全計算機平臺的構(gòu)建具有十分重要的理論與實際意義。因此,本文旨在提出下一代列控安全計算機平臺的結(jié)構(gòu)與具體實現(xiàn)功能的基礎(chǔ)上,對其中的管理機制進行驗證,并進行管理單元的設(shè)計與實現(xiàn)。在對國內(nèi)外列控系統(tǒng)進行研究的基礎(chǔ)上,本文分析了下一代列控安全計算機功能需求,并對其內(nèi)部結(jié)構(gòu)進行詳細說明,對集中式系統(tǒng)進行了結(jié)構(gòu)上的改進,提出了分布式系統(tǒng)結(jié)構(gòu)的下一代列控安全計算機設(shè)計方案,并對其管理域所實現(xiàn)的控制機制以及其原理進行設(shè)計,提出了內(nèi)部單元的具體功能需求及運行流程。根據(jù)其所實現(xiàn)的管理功能,通過CTL操作符對相關(guān)性質(zhì)進行描述,并以SMV描述語言對其進行狀態(tài)機模型的建立,通過所選取的NuSMV形式化驗證工具對其所實現(xiàn)的管理機制進行了相關(guān)性質(zhì)的形式化驗證,并對驗證結(jié)果進行了分析,證明所設(shè)計的管理機制符合設(shè)計規(guī)范。硬件設(shè)計方面,基于差異性設(shè)計的原則,本文主要對管理域中基于MCU實現(xiàn)的管理單元進行設(shè)計。根據(jù)其具體的功能需求,完成了硬件相關(guān)模塊的設(shè)計,并進行了MCU邏輯板PCB圖的繪制。軟件測試方面,通過編程對管理單元內(nèi)部的狀態(tài)機進行軟件實現(xiàn),并以PC機模擬FPGA邏輯板,實現(xiàn)其與MCU邏輯板的數(shù)據(jù)交互過程,通過設(shè)計的狀態(tài)監(jiān)測器對狀態(tài)機內(nèi)部進行監(jiān)測。同時,以故障注入的方式對其所實現(xiàn)的狀態(tài)轉(zhuǎn)移功能進行了測試。通過對測試結(jié)果的分析,本文所設(shè)計與實現(xiàn)的基于MCU的管理單元能夠?qū)崿F(xiàn)預(yù)期的控制機制,實現(xiàn)了最初的設(shè)計目標。
【關(guān)鍵詞】：列控 安全計算機 管理機制 形式化驗證 設(shè)計與實現(xiàn)
【學(xué)位授予單位】：北京交通大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：U284.48
【目錄】：

• 致謝5-6
• 摘要6-7
• ABSTRACT7-11
• 1 引言11-19
• 1.1 選題背景及意義11-16
• 1.1.1 列控系統(tǒng)概述11-15
• 1.1.2 列控安全計算機的應(yīng)用15-16
• 1.1.3 本文研究意義16
• 1.2 國內(nèi)外研究現(xiàn)狀16-18
• 1.3 論文研究內(nèi)容和組織結(jié)構(gòu)18
• 1.4 本章小結(jié)18-19
• 2 列控安全計算機管理機制設(shè)計19-37
• 2.1 列控安全計算機概述19-25
• 2.1.1 列控安全計算機功能需求19-20
• 2.1.2 既有列控安全計算機平臺結(jié)構(gòu)20-22
• 2.1.3 下一代列控安全計算機結(jié)構(gòu)22-25
• 2.2 列控安全計算機控制原理25-28
• 2.2.1 列控安全計算機功能描述25-26
• 2.2.2 基于通信的任務(wù)級同步策略26-27
• 2.2.3 數(shù)據(jù)比較功能27-28
• 2.3 系統(tǒng)運行流程28-35
• 2.3.1 主備狀態(tài)切換流程28-32
• 2.3.2 管理單元運行流程32-35
• 2.4 本章小結(jié)35-37
• 3 安全計算機管理機制的形式化驗證37-71
• 3.1 形式化驗證方法37-43
• 3.1.1 模型檢驗原理及步驟37-39
• 3.1.2 CTL計算樹邏輯概述39-42
• 3.1.3 模型檢測工具42-43
• 3.2 管理單元的SMV建模43-54
• 3.2.1 管理單元狀態(tài)模型43-48
• 3.2.2 程序結(jié)構(gòu)及模型轉(zhuǎn)換規(guī)則48-54
• 3.3 驗證結(jié)果分析54-70
• 3.4 本章小結(jié)70-71
• 4 安全計算機管理單元的實現(xiàn)與測試71-97
• 4.1 管理單元的硬件設(shè)計與實現(xiàn)71-84
• 4.1.1 管理單元的硬件結(jié)構(gòu)和功能71
• 4.1.2 硬件各模塊的設(shè)計71-82
• 4.1.3 PCB電路板的實現(xiàn)82-84
• 4.2 狀態(tài)機的設(shè)計與軟件實現(xiàn)84-88
• 4.2.1 安全軟件的實現(xiàn)84-86
• 4.2.2 狀態(tài)機軟件程序?qū)崿F(xiàn)86-88
• 4.3 調(diào)試環(huán)境設(shè)計與實現(xiàn)88-91
• 4.4 測試結(jié)果分析91-95
• 4.5 本章小結(jié)95-97
• 5 結(jié)論97-99
• 5.1 總結(jié)97-98
• 5.2 展望98-99
• 參考文獻99-103
• 附錄A103-105
• 圖索引105-107
• 表索引107-108
• 作者簡歷及攻讀碩士學(xué)位期間取得的研究成果108-110
• 學(xué)位論文數(shù)據(jù)集110

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

1 袁湘鄂;史增樹;李智;;盡頭式車站列控技術(shù)方案[J];鐵道通信信號;2010年08期

2 程憶佳;王俊峰;;列控數(shù)據(jù)完備性建模方法研究[J];鐵路計算機應(yīng)用;2012年07期

3 康健;黨建武;趙庶旭;;客運專線列控設(shè)備維修研究[J];中國鐵路;2012年09期

4 康健;周振華;;基于費用最小的列控設(shè)備維修優(yōu)化與仿真[J];鐵道標準設(shè)計;2012年12期

5 魏方華;吳倩;劉瀾;;一次模式曲線列控方式追蹤間隔的模擬計算與優(yōu)化設(shè)計[J];交通運輸系統(tǒng)工程與信息;2007年03期

6 閆曉莉;;列控車載數(shù)據(jù)無線傳輸管理系統(tǒng)的運用[J];鐵道通信信號;2012年09期

7 易磊;郭友強;;列控車載設(shè)備維護管理探討[J];鐵道通信信號;2013年03期

8 張?zhí)?;淺析非安全通道傳輸列控安全信息的措施和方法[J];甘肅科技縱橫;2008年04期

9 徐建軍;;鐵路客專樞紐列控地面設(shè)備布置方案研究[J];鐵道通信信號;2011年11期

10 傅世善;;閉塞與列控概論——第一講 區(qū)間閉塞[J];鐵路通信信號工程技術(shù);2004年05期

中國重要會議論文全文數(shù)據(jù)庫 前3條

1 謝靜高;石銳華;;客運專線列控系統(tǒng)技術(shù)方案的探討[A];鐵路客運專線建設(shè)技術(shù)交流會論文集[C];2005年

2 李桂月;張洲初;牛意堅;;GSM-R網(wǎng)絡(luò)列控類數(shù)據(jù)傳輸業(yè)務(wù)的QoS測試[A];GSM-R移動通信及無線電管理學(xué)術(shù)會議論文集[C];2006年

3 徐偉;肖寶弟;;基于多任務(wù)融合的城軌車載維檢系統(tǒng)的設(shè)計與實現(xiàn)[A];第七屆中國智能交通年會優(yōu)秀論文集——智能交通應(yīng)用[C];2012年

中國重要報紙全文數(shù)據(jù)庫 前2條

1 譚小兵邋蘇元宏;我國首套鐵路信號、列控地面系統(tǒng)試驗成功[N];人民鐵道;2007年

2 中國鐵道科學(xué)研究院 蔣志勇;無線通信在高速鐵路的應(yīng)用[N];人民郵電;2012年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前8條

1 張勇;列控設(shè)備開發(fā)項目安全風(fēng)險管理研究[D];浙江工業(yè)大學(xué);2014年

2 梁靚;列控安全計算機管理機制的形式化驗證與實現(xiàn)[D];北京交通大學(xué);2016年

3 魏方華;基于模式曲線列控方式的列車追蹤行車模擬研究[D];西南交通大學(xué);2005年

4 殷原;提速條件下山區(qū)鐵路列控方式研究[D];西南交通大學(xué);2007年

5 裴麗君;列控模型參數(shù)辨識及其在線學(xué)習(xí)算法研究[D];北京交通大學(xué);2011年

6 陳耿欽;基于MAS的列控系統(tǒng)安全分析平臺架構(gòu)和關(guān)鍵算法研究[D];北京交通大學(xué);2014年

7 薛輝;基于UML的車載列控顯示系統(tǒng)的設(shè)計與實現(xiàn)[D];北京交通大學(xué);2006年

8 李e，

本文編號：414807