第1章列車運行控制繫統實時性概述1

1.1列車運行控制繫統簡介1

1.1.1列車運行控制繫統的現狀與發展1

1.1.2列車運行控制繫統的組成2

1.1.3列車運行控制繫統的特點3

1.2列車運行控制繫統的實時性要求5

1.3國內外研究現狀6

1.4列車運行控制繫統實時性的建模與驗證方法8

第2章基於UML的列控繫統實時性研究10

2.1UML概述10

2.1.1UML的定義10

2.1.2UML的組成10

2.1.3UML建模機制14

2.2UML擴展機制15

2.2.1約束15

2.2.2標記值16

2.2.3構造型17

2.3列控繫統的UML模型18

2.3.1用例圖18

2.3.2類圖19

2.3.3活動圖21

2.3.4部署圖22

2.3.5序列圖23

2.3.6狀態圖26

2.4基於UML的模型轉換方法29

2.4.1模型轉換的概念30

2.4.2模型31

第3章基於UML與CSP的實時繫統建模與分析35

3.1CSP相關理論36

3.1.1CSP的語法和語義36

3.1.2CSP的實時性擴展37

3.2UML到CSP的轉換規則39

3.2.1活動圖轉換規則39

3.2.2狀態圖轉換規則41

3.3模型轉換中特性的保持與轉換規則的證明45

3.3.1模型轉換中特性的保持45

3.3.2模型轉換規則的證明46

3.4UML轉換至CSP的列控繫統實時性分析實例50

第4章基於時間自動機的繫統建模與驗證53

4.1時間自動機53

4.1.1時間約束和時間解釋53

4.1.2時間語言55

4.1.3時間自動機的語義55

4.1.4時間自動機的積57

4.2基於時間自動機的形式化建模58

4.3模型檢驗方法驗證實時繫統59

4.3.1時序邏輯60

4.3.2時序邏輯的時間化62

4.3.3驗證流程64

4.4定理證明方法驗證實時繫統65

4.5基於時間自動機的列控繫統模型實例67

4.5.1案例描述67

4.5.2案例模型的時間約束68

4.5.3案例建模與驗證分析69

第5章基於著色Petri網的繫統建模與分析72

5.1著色Petri網72

5.1.1Petri網概述72

5.1.2Petri網的結構73

5.1.3Petri網的行為特性74

5.1.4著色Petri網的定義76

5.2基於著色Petri網的復雜繫統實時性任務的建模及其分析77

5.2.1復雜繫統結構和實時性任務的基本假設77

5.2.2基於著色Petri網的復雜繫統實時性任務建模78

5.2.3基於著色Petri網模型的復雜繫統實時性任務的可靠性分析79

5.2.4著色Petri網中復雜繫統實時性評價方法80

5.3基於著色Petri網的列控繫統分析實例82

5.3.1實例描述82

5.3.2CPN模型的建立85

5.3.3時間模型的建立與驗證91

第6章基於馬爾可夫鏈的實時繫統分析94

6.1馬爾可夫鏈理論94

6.1.1馬爾可夫鏈94

6.1.2狀態轉移95

6.1.3馬爾可夫分析96

6.2馬爾可夫鏈在列車行車時間預測中的應用98

6.2.1隱馬爾可夫鏈98

6.2.2自回歸模型算法99

6.2.3時間性和關聯性聚類算法100

6.2.4維特比算法102

6馬爾可夫鏈與列控繫統信息時效性評價104

6.3.1列控繫統的信息時效性判定104

6.3馬爾可夫鏈模型的構造109

6.3.3模型參數的估計111

參考文獻115

隨著經濟實力和科技水平的不斷提高，我國高速鐵路的發展取得了舉世矚目的成就，已經擁有了水平的基於通信的列車運行控制繫統。傳統的基於軌道電路的列車運行控制繫統，其傳輸信息量少，受環境影響大，而基於通信的列車運行控制繫統（以下簡稱列控繫統），采用GSMR無線通信繫統，實現地面與車載設備之間實時、連續、雙向、大容量的信息傳輸，滿足列車運行要求，適應我國高速鐵路高速度、高密度及不同速度等級列車跨線運行，還具有建設成本低、運營效率高和運行安全等優點，成為未來列控繫統發展的方向。

列控繫統也是一個典型的安全苛求繫統，繫統的硬件、軟件安全性級別要求很高，繫統的任何故障都可能導致人員傷亡、重大經濟損失或環境破壞。

鐵路通信安全標準EN 501592指出：如果安全苛求繫統包括跨區域的信息交換，那麼通信繫統就成為安全相關繫統的一部分，它必須保證端到端通信的安全性和實時性。可見，實時性是列控繫統的重要特點，實時性除了要求繫統能夠作出正確的響應外，還要求繫統響應事件的順序也正確，並且必須在規定的時間內作出響應。在《CTCS3級列控繫統總體技術方案》和《CTCS3級列控繫統——繫統需求規範》等規範文件中有大量對列控繫統實時性要求的條款，比如：“車載設備應在40秒內注冊GSMR並建立可靠連接”“時間大於10秒應被認為車載與無線閉塞中心（RBC）建立連接失敗”“自動轉換後5秒內司機應進行確認，如果司機不確認，將對其非正常操作進行記錄等”。因此，研究列控繫統的實時性是非常必要的。

本書繫統地介紹了列車運行控制繫統實時性的特點，以及建模與驗證方法。重點闡述了基於UML、CSP、時間自動機、著色Petri網、馬爾可夫鏈等理論和方法的列控繫統，探討了實現列控繫統實時性建模與驗證所必須的理論與關鍵技術。在應用方面，介紹了支持相關研究方法的技術手段及其算法。

本書的研究工作是在國家自然科學基金項目“基於交互式馬爾可夫鏈的列車運行控制繫統安全通信實時性的研究”（項目批準號：61703028）和北京市屬高校基本科研業務費項目“基於CPS的建築智能化繫統網絡安全性研究”（項目批準號：X18071）的聯合資助下完成的，在此表示衷心的感謝。

在本書的撰寫過程中，得到了北京交通大學軌道交通控制與安全國家重點實驗室、北京建築大學電氣與信息工程學院廣大師生的大力支持和協助，對所有審閱本書以及在本書的寫作和出版過程中給予熱情幫助的朋友們表示衷心感謝。

由於作者水平有限，書中難免存在不妥之處，懇請同仁和讀者批評指正。

作者

2018年12月於北京