中國列車運行控制系統(tǒng)（Chinese20Train20Control20System,CTCS）是保障列車運行安全和效率的安全苛求系統(tǒng)。列控數(shù)據(jù)作為信號設(shè)備信息、列車狀態(tài)信息和線路信息的載體,其正確性是列車安全運行的重要前提。目前針對不同的列控子系統(tǒng),數(shù)據(jù)描述方式不同且沒有特定的數(shù)據(jù)規(guī)范,列控數(shù)據(jù)的驗證也主要依靠人工校驗和仿真測試相結(jié)合的方式,效率低且正確性難以保證。針對上述問題,本文以研究CTCS-1級列控系統(tǒng)地面核心設(shè)備—區(qū)域列控數(shù)據(jù)中心（RDC）的靜態(tài)數(shù)據(jù)驗證為例,從RDC數(shù)據(jù)組織方式設(shè)計和數(shù)據(jù)驗證兩個方面進行了研究,首先建立了20RDC靜態(tài)數(shù)據(jù)模型,然后提出了數(shù)據(jù)驗證的總體框架,設(shè)計和開發(fā)了20RDC數(shù)據(jù)自動化驗證工具,實現(xiàn)了數(shù)據(jù)的自動化驗證。論文完成的工作包括:（1）設(shè)計RDC數(shù)據(jù)組織方式,建立RDC靜態(tài)數(shù)據(jù)模型。通過分析RDC系統(tǒng)需求將數(shù)據(jù)分為點元素、線元素和區(qū)域元素,構(gòu)建各數(shù)據(jù)元素之間的邏輯關(guān)系模型,使之既體現(xiàn)線路拓撲關(guān)系又便于后期維護和更新,最終建立RDC靜態(tài)數(shù)據(jù)結(jié)構(gòu)模型,并結(jié)合實際線路數(shù)據(jù)生成RDC靜態(tài)數(shù)據(jù)庫。（2）提出數(shù)據(jù)建模和驗證的總體框架,將其分為四個階段:數(shù)據(jù)... 

【文章來源】：北京交通大學北京市 211工程院校 教育部直屬院校

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

【學位級別】：碩士

【文章目錄】：
致謝
摘要
ABSTRACT
1 引言
    1.1 研究背景和意義
        1.1.1 研究背景
        1.1.2 選題目的及意義
    1.2 數(shù)據(jù)驗證研究現(xiàn)狀
        1.2.1 列控系統(tǒng)數(shù)據(jù)驗證研究現(xiàn)狀
        1.2.2 其他領(lǐng)域數(shù)據(jù)驗證研究現(xiàn)狀
    1.3 CTCS-1級列控系統(tǒng)概述
    1.4 論文的研究內(nèi)容和框架
2 數(shù)據(jù)驗證的理論基礎(chǔ)
    2.1 數(shù)據(jù)設(shè)計模型概述
    2.2 通信順序進程形式化建模方法
        2.2.1 CSP方法概述
        2.2.2 通信順序進程CSP語義和語法
    2.3 CSP模型-Petri網(wǎng)模型轉(zhuǎn)換方法
        2.3.1 Petri網(wǎng)基本概念
        2.3.2 CSP-Petri網(wǎng)模型轉(zhuǎn)換規(guī)則
    2.4 本章小結(jié)
3 RDC靜態(tài)數(shù)據(jù)生成
    3.1 RDC概述
    3.2 RDC靜態(tài)數(shù)據(jù)需求分析
    3.3 RDC數(shù)據(jù)組織方式分析
    3.4 RDC靜態(tài)數(shù)據(jù)模型建立
    3.5 RDC靜態(tài)數(shù)據(jù)生成實例
    3.6 本章小結(jié)
4 RDC數(shù)據(jù)驗證CSP模型的建立
    4.1 RDC數(shù)據(jù)驗證總體框架
    4.2 RDC數(shù)據(jù)建模驗證的總體思路
    4.3 數(shù)據(jù)約束規(guī)則提取和驗證方法設(shè)計
        4.3.1 數(shù)據(jù)約束規(guī)則提取
        4.3.2 約束規(guī)則管理
        4.3.3 數(shù)據(jù)驗證方法設(shè)計
    4.4 數(shù)據(jù)驗證CSP模型
        4.4.1 數(shù)據(jù)驗證總體模型
        4.4.2 驗證軌道區(qū)段數(shù)據(jù)CSP模型
        4.4.3 驗證進路數(shù)據(jù)CSP模型
    4.5 本章小結(jié)
5 數(shù)據(jù)驗證模型的形式化驗證
    5.1 模型檢驗方法
    5.2 驗證工具ProB
        5.2.1 ProB概述
        5.2.2 CSP_M語言轉(zhuǎn)換
    5.3 CSP語義模型檢驗
        5.3.1 性質(zhì)驗證分析
        5.3.2 數(shù)據(jù)驗證模型正確性檢驗
        5.3.3 數(shù)據(jù)驗證模型功能性檢驗
        5.3.4 數(shù)據(jù)驗證模型安全性檢驗
        5.3.5 驗證結(jié)果分析
    5.4 本章小結(jié)
6 RDC數(shù)據(jù)自動化驗證工具的設(shè)計與實現(xiàn)
    6.1 需求分析
    6.2 軟件設(shè)計
        6.2.1 軟件總體設(shè)計
        6.2.2 數(shù)據(jù)審核邏輯模塊詳細設(shè)計
    6.3 軟件實現(xiàn)
        6.3.1 開發(fā)環(huán)境
        6.3.2 軟件主界面
    6.4 實際線路數(shù)據(jù)驗證
    6.5 本章小結(jié)
7 結(jié)論
    7.1 總結(jié)
    7.2 展望
參考文獻
圖索引
表索引
作者簡歷及攻讀碩士學位期間取得的研究成果
學位論文數(shù)據(jù)集


【參考文獻】：
期刊論文
[1]高速鐵路產(chǎn)業(yè)發(fā)展的區(qū)域布局研究——基于中國鐵路中長期發(fā)展規(guī)劃政策[J]. 閆昱霖.  經(jīng)濟師. 2017(11)
[2]列車運行控制數(shù)據(jù)校核及管理系統(tǒng)[J]. 呂瑞,馬春英.  鐵道通信信號. 2017(02)
[3]基于SAT的應(yīng)答器工程數(shù)據(jù)邏輯規(guī)則提取及驗證[J]. 王彤典,趙會兵.  鐵道學報. 2017(02)
[4]CTCS-1級列控系統(tǒng)總體技術(shù)方案探討[J]. 莫志松.  中國鐵路. 2016(08)
[5]城軌計算機聯(lián)鎖的數(shù)據(jù)安全性驗證[J]. 周果,趙會兵.  鐵道學報. 2016(08)
[6]列控工程數(shù)據(jù)自動審核的研究與實現(xiàn)[J]. 陳倩佳,盧佩玲.  鐵路計算機應(yīng)用. 2015(03)
[7]CTCS-0列控系統(tǒng)改造方案研究[J]. 黃玉祥.  中國鐵路. 2014(09)
[8]基于進程跡的CSP模型驗證框架[J]. 趙嶺忠,翟仲毅,錢俊彥.  計算機科學. 2013(11)
[9]列控數(shù)據(jù)完備性建模方法研究[J]. 程憶佳,王俊峰.  鐵路計算機應(yīng)用. 2012(07)
[10]CTCS-1級列控系統(tǒng)車載設(shè)備研發(fā)探討[J]. 宮建基.  鐵路技術(shù)創(chuàng)新. 2012(02)

博士論文
[1]基于SCBM的安全分析方法及其在列控系統(tǒng)中的應(yīng)用[D]. 周果.北京交通大學 2016

碩士論文
[1]基于CSP的PSTM框架形式化分析與驗證[D]. 劉艾倫.華東師范大學 2018
[2]基于TCPN的CTCS-1級列控系統(tǒng)RDC形式化建模與分析[D]. 徐越.北京交通大學 2018
[3]列控數(shù)據(jù)計算機輔助設(shè)計與驗證方法研究[D]. 馮丹穎.北京交通大學 2018
[4]基于CSP的CBTC系統(tǒng)區(qū)域控制器的建模與驗證[D]. 朱葛.北京交通大學 2014
[5]基于UPPAAL的CBTC系統(tǒng)數(shù)據(jù)驗證的研究[D]. 王森.北京交通大學 2013
[6]基于STATEMATE的無線閉塞中心數(shù)據(jù)流生成及形式化驗證[D]. 秦玲.北京交通大學 2009
[7]Petri網(wǎng)的改良可達樹及可達性判定[D]. 邱經(jīng)華.山東科技大學 2004



本文編號：3178896