列车运行控制系统实时性的建模与验证

     本书是对目前列车控制系统实时性研究的进一步推进与深化，针对不同的问题与侧重点，从不同角度，用多种方法对系统的实时性展开研究。 

     本书系统地介绍了列车运行控制系统实时性的特点，以及建模与验证方法。重点阐述了基于UML、CSP、时间自动机、着色Petri网、马尔可夫链等理论和方法的列控系统，探讨了实现列控系统实时性建模与验证所必须的理论与关键技术。在应用方面，介绍了支持相关研究方法的技术手段及其算法。本书适合作为高等院校铁路信号及相关专业的教学参考用书，也可供相关领域研究人员参考。

     谢雨飞，男，任教于北京建筑大学电气与信息工程学院。主要研究方向：复杂系统建模与求解、网络安全技术等，主持国家自然基金项目1项，发表EI、核心期刊论文10余篇。

第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.2UML元模型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.3多元马尔可夫链与列控系统信息时效性评价104

6.3.1列控系统的信息时效性判定104

6.3.2多元马尔可夫链模型的构造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月于北京