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

【文章來(lái)源】：北京交通大學(xué)北京市 211工程院校 教育部直屬院校

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

【學(xué)位級(jí)別】：碩士

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


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

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

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



本文編號(hào)：3178896