與航空、公路等交通方式相比,鐵路運輸具有運量大、環(huán)境友好、準點率高等優(yōu)點,使得鐵路運輸在各國交通運輸體系中占有重要的地位。列車運行控制系統(tǒng)是鐵路信號的重要組成部分,是保障行車安全、提高運輸效率和行車速度的關鍵子系統(tǒng)。隨著我國"一帶一路"的戰(zhàn)略的實施,如何滿足互聯(lián)互通需求和安全技術保障成為了鐵路信號領域所關注的問題。ETCS是為實現(xiàn)互聯(lián)互通而制定的列控技術規(guī)范,其中ETCS-1級與ETCS-NTC級之間的等級轉換是歐洲列控系統(tǒng)和本國列控系統(tǒng)之間的轉換,因此對兩者之間等級轉換的研究非常有必要。通過形式化模型對系統(tǒng)進行設計和驗證,可以保證系統(tǒng)設計開發(fā)的正確性和安全性。本文在對ETCS系統(tǒng)需求規(guī)范、專用傳輸模塊接口規(guī)范、互聯(lián)互通性能要求規(guī)范進行需求分析的基礎上,建立了 ETCS-1/ETCS-NTC等級轉換的列控車載設備、軌旁單元和系統(tǒng)環(huán)境間信息交互的時間自動機模型,最后對模型進行仿真和形式化驗證。首先,從系統(tǒng)功能架構和系統(tǒng)應用等級方面對ETCS進行了介紹,闡述了 ETCS的適用范圍、系統(tǒng)組成、系統(tǒng)環(huán)境和應用現(xiàn)狀。其次,對列控車載設備從開始任務進入ETCS-1級、到與專用傳輸模塊連接,ETCS... 

【文章來源】：西南交通大學四川省 211工程院校 教育部直屬院校

【文章頁數(shù)】：70 頁

【學位級別】：碩士

【文章目錄】：
摘要
Abstract
第1章 緒論
    1.1 研究背景和意義
    1.2 國內外研究現(xiàn)狀
        1.2.1 國內現(xiàn)狀
        1.2.2 國外現(xiàn)狀
    1.3 論文的主要工作
第2章 系統(tǒng)建模和形式化方法
    2.1 系統(tǒng)建模與驗證
        2.1.1 建模方法
        2.1.2 驗證方法
    2.2 基于時間自動機的建模
        2.2.1 狀態(tài)轉移系統(tǒng)
        2.2.2 時間自動機的語義和語法:
        2.2.3 時間自動機網絡
    2.3 模型驗證工具UPPAAL
        2.3.1 UPPAAL的結構和特征
        2.3.2 UPPAAL的描述語言
    2.4 本章小結
第3章 ETCS-1/ETCS-NTC等級轉換建模
    3.1 ETCS列控系統(tǒng)概述
        3.1.1 系統(tǒng)結構
        3.1.2 應用等級
    3.2 列車進入ETCS-1級與STM連接
        3.2.1 開始任務場景分析
        3.2.2 開始任務進入ETCS-1級模型
        3.2.3 STM與ETCS連接場景分析
        3.2.4 STM與ETCS連接模型
    3.3 ETCS-1向ETCS-NTC轉換
        3.3.1 場景分析
        3.3.2 ETCS-1向ETCS-NTC轉換模型
    3.4 ETCS-NTC向ETCS-1轉換
        3.4.1 場景分析
        3.4.2 ETCS-NTC向ETCS-1轉換模型
    3.5 本章小結
第4章 模型的驗證分析
    4.1 仿真驗證
    4.2 形式化驗證
        4.2.1 功能需求的驗證
        4.2.2 安全性的驗證
        4.2.3 時間約束的驗證
    4.3 本章小結
總結
致謝
參考文獻



本文編號：3069558