車載功能兼容研究主要解決的是列車跨線運行的問題,其一是通過合理的系統(tǒng)功能設計,使車載系統(tǒng)能支持列車在低等級線路條件下的安全運行控制,其二是通過合理的場景設計,使面臨跨線運行的列車能安全且高效地實現(xiàn)在不同控制等級之間的轉換。CTCS-1級列控系統(tǒng)總體技術方案中提出了在車載系統(tǒng)內部集成C0級系統(tǒng)功能的設想,而項目的前期工作集中于C1級系統(tǒng)的核心業(yè)務功能,未能對C1/C0的車載功能兼容問題給出明確方案。對此,本文總結了當前C1車載功能兼容方案中存在的問題,并對當前方案進行了優(yōu)化設計。提出了針對功能兼容方案的建模與驗證框架,建立了功能兼容方案的基礎模型,并綜合利用NuSMV符號模型檢驗技術和TCPN建模與仿真方法,從系統(tǒng)功能設計和列車運營場景兩個維度,對優(yōu)化后的功能兼容方案進行了驗證。本文完成的主要工作如下:（1）C1車載功能兼容需求分析與方案的優(yōu)化設計。梳理了 C1級列控系統(tǒng)規(guī)范文檔中功能兼容相關內容,對核心控制單元的交互方案進行了比選,確定其一為本文的研究基礎;通過系統(tǒng)功能分析,提取了 C1/C0車載功能兼容需求;從車載系統(tǒng)結構、功能單元交互等方面對現(xiàn)有方案進行了優(yōu)化。（2）方案驗證研究框... 

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

【學位級別】：碩士

【文章目錄】：
致謝
摘要
ABSTRACT
1 引言
    1.1 研究背景
    1.2 國內外研究現(xiàn)狀
        1.2.1 CTCS-1級列控系統(tǒng)的研究現(xiàn)狀
        1.2.2 列控系統(tǒng)向下兼容問題的研究現(xiàn)狀
        1.2.3 形式化方法在列控領域的應用
    1.3 研究目的與意義
    1.4 論文內容與組織結構
2 CTCS-1級列控車載功能兼容方案優(yōu)化設計
    2.1 CTCS-1級列控車載功能兼容方案分析
        2.1.1 當前兼容方案存在的問題
        2.1.2 核心控制單元交互設計比選
    2.2 CTCS-1級列控車載功能兼容需求分析
        2.2.1 CTCS-0和CTCS-1級系統(tǒng)功能分析
        2.2.2 CTCS-1級列控系統(tǒng)的功能兼容需求
        2.2.3 功能兼容需求管理
    2.3 CTCS-1級列控車載功能兼容方案優(yōu)化
        2.3.1 車載系統(tǒng)總體設計
        2.3.2 車載主機內部功能單元設計
        2.3.3 車載接口設計
    2.4 本章小結
3 CTCS-1級列控車載功能兼容方案建模
    3.1 功能兼容方案建模與驗證框架
        3.1.1 基于模型的方案驗證思路
        3.1.2 功能兼容方案的抽象方法
    3.2 CTCS-1級列控車載系統(tǒng)建模
        3.2.1 車載系統(tǒng)的類模型
        3.2.2 車載主機內部功能單元的行為模型
        3.2.3 車載主機內部功能單元的交互模型
    3.3 CTCS-1級列控車載核心功能建模
        3.3.1 速度計算與列車定位流程
        3.3.2 運行控制曲線計算流程
        3.3.3 速度監(jiān)控與防護輸出流程
    3.4 本章小結
4 CTCS-1級列控車載功能兼容方案驗證
    4.1 CTCS-1級車載功能兼容方案驗證方法
        4.1.1 NuSMV概述
        4.1.2 基于UML的NuSMV建模與驗證方法
    4.2 功能兼容方案的NuSMV模型
        4.2.1 UML-NuSMV模型轉換規(guī)則
        4.2.2 NuSMV模型的子模塊
        4.2.3 NuSMV模型的主模塊
    4.3 待驗證屬性的提取與CTL描述
        4.3.1 待驗證屬性的提取
        4.3.2 待驗證屬性的描述方法
    4.4 驗證結果與分析
        4.4.1 驗證結果
        4.4.2 驗證分析
    4.5 本章小結
5 CTCS-1/CTCS-0等級轉換場景設計與驗證
    5.1 CTCS-0/CTCS-1等級轉換場景
        5.1.1 CTCS-1/CTCS-0等級轉換需求分析
        5.1.2 CTCS-0至CTCS-1的等級轉換場景
        5.1.3 CTCS-1至CTCS-0的等級轉換場景
    5.2 TCPN建模與仿真分析方法
        5.2.1 時間有色Petri網
        5.2.2 基于UML的TCPN建模與仿真分析方法
    5.3 CTCS-0/CTCS-1等級轉換場景的CPN建模
        5.3.1 等級轉換場景的頂層模型
        5.3.2 等級轉換場景的子模型
        5.3.3 模型的動態(tài)特性驗證
    5.4 CTCS-0/CTCS-1等級轉換場景仿真
        5.4.1 等級轉換場景的TCPN模型
        5.4.2 仿真結果分析
    5.5 本章小結
6 總結與展望
    6.1 論文總結
    6.2 研究展望
參考文獻
圖索引
表索引
作者簡歷及攻讀碩學位期間取得的研究成果
學位論文數(shù)據(jù)集


【參考文獻】：
期刊論文
[1]基于增強型BN的CTCS-1級ATP可靠性研究[J]. 劉中田,徐越,王昊.  北京交通大學學報. 2017(05)
[2]CTCS-1級列控系統(tǒng)總體技術方案探討[J]. 莫志松.  中國鐵路. 2016(08)
[3]城軌CBTC系統(tǒng)聯(lián)鎖表數(shù)據(jù)安全邏輯驗證方法研究[J]. 張淼,黃友能,任嘯宇.  鐵路計算機應用. 2015(05)

博士論文
[1]列車運行控制系統(tǒng)安全通信協(xié)議驗證方法的研究[D]. 陳黎潔.北京交通大學 2013
[2]列控系統(tǒng)需求規(guī)范形式化建模與驗證方法研究[D]. 謝雨飛.北京交通大學 2012
[3]高速鐵路列車運行控制系統(tǒng)的形式化建模與驗證方法研究[D]. 曹源.北京交通大學 2011
[4]軌道交通列車運行控制系統(tǒng)的形式化建模和模型檢驗方法研究[D]. 燕飛.北京交通大學 2006

碩士論文
[1]CTCS-1級列控系統(tǒng)車載設備安全性分析[D]. 王昊.北京交通大學 2017
[2]基于隨機Petri網的高鐵列控系統(tǒng)C2/C3等級轉換過程建模及仿真[D]. 王建.西南交通大學 2015
[3]基于Event-B的聯(lián)鎖系統(tǒng)進路控制建模與驗證研究[D]. 童湖東.北京交通大學 2013
[4]基于規(guī)則的CBTC系統(tǒng)數(shù)據(jù)分析與驗證的研究[D]. 董秋麗.北京交通大學 2012



本文編號：3702644