第1章 绪论 1
1.1 列车运行安全背景及意义 1
1.2 基于无线通信的列车运行控制系统 5
1.2.1 列车运行控制系统构成与分类 5
1.2.2 CTCS列控系统 7
1.2.3 GSM-R铁路无线通信系统 10
1.3 列车控制形式化研究现状 11
1.4 本书内容与结构安排 14
第2章 形式化建模理论与复杂系统理论 17
2.1 建模基本理论 17
2.1.1 系统、模型、仿真的基本概念 17
2.1.2 系统模型的分类 18
2.1.3 建模方法的分类 19
2.1.4 建模的一般原则 19
2.1.5 建模步骤的划分 19
2.2 形式化理论 21
2.2.1 形式化概念 21
2.2.2 形式化分类 22
2.2.3 形式化验证方法 23
2.2.4 常见的形式化建模方法 24
2.3 复杂系统建模理论 25
2.3.1 复杂系统 25
2.3.2 复杂适应系统理论 26
2.3.3 分布式人工智能 28
2.3.4 多智能体基础理论 28
2.4 Event-B方法及Rodin平台 30
2.4.1 Event-B基本结构 30
2.4.2 Event-B数学体系 32
2.4.3 Event-B模型精化和证明义务 35
2.4.4 RODIN平台 37
本章小结 38
第3章 交通系统建模 39
3.1 交通系统仿真 39
3.1.1 交通系统仿真基本概念 39
3.1.2 系统分类与系统模型 40
3.2 交通流理论 40
3.2.1 交通流理论分类 41
3.2.2 交通流理论参数 41
3.2.3 交通流主要研究内容 44
3.3 交通多分辨率建模方法 45
3.3.1 宏观交通建模仿真 45
3.3.2 微观交通建模仿真 45
3.3.3 中观交通建模仿真 45
本章小结 46
第4章 CTCS-4级车地通信机制的形式化研究 47
4.1 通信顺序进程形式化理论基础 47
4.1.1 通信与递归 48
4.1.2 C SP的运算符 49
4.1.3 过程行为 49
4.1.4 进程的迹 49
4.1.5 CSP模型检测工具 50
4.1.6 故障发散检测器FDR 50
4.2 基于MAS的RBC切换场景描述及车地通信信息交互流的实现 52
4.2.1 列控系统多Agent系统抽象 53
4.2.2 基于CPN的混合Agent模型 54
4.2.3 MAS模型形式化定义 55
4.2.4 基于CORBA的发布订阅模式的车地通信 56
4.3 基于CSP的车地实时通信协议形式化建模与验证 58
4.3.1 MAS系统通信协议形式化验证框架 58
4.3.2 列控系统实时通信协议的形式化建模 59
4.3.3 CSP语言对车地实时通信协议建模 60
4.3.4 Casper＋FDR对实时通信协议验证 64
4.4 注入故障的Agent通信模型 65
4.4.1 故障导向安全性功能分析与验证 67
4.4.2 列控系统消息处理实时性分析 68
4.4.3 通信时效性分析 69
本章小结 70
第5章 基于S PN的高可信无线通信形式化建模与分析 71
5.1 Petri网形式化方法 72
5.1.1 Petri网的数学定义 73
5.1.2 SPN基本概念 74
5.1.3 SPN变迁激活规则 75
5.1.4 Petri网建模事件类型 76
5.1.5 Petri网基本性质 78
5.2 无线通信系统 79
5.2.1 GSM-R描述 79
5.2.2 列车控制数据传输业务QoS指标 80
5.3 高可信无线通信SPN模型 82
5.4 通信机制SPN模型 83
5.5 通信故障恢复SPN模型 84
5.6 仿真实验 88
5.6.1 软件仿真工具TimeNET 88
5.6.2 扩展确定性随机Petri网理论 89
5.6.3 MOSEL编程语法 90
5.6.4 仿真分析 91
本章小结 94
第6章 基于细胞膜计算的无线通信并行形式化建模 95
6.1 细胞膜的化学组成和结构 96
6.1.1 细胞膜组成结构 96
6.1.2 物质的跨膜运输 97
6.2 膜计算基本概念与基础知识 99
6.2.1 细胞膜计算方法 99
6.2.2 马尔科夫过程 101
6.3 基于生化反应速率的膜计算方法 101
6.4 细胞膜计算方法在无线通信系统中的仿真应用 102
6.4.1 ETCS无线通信系统 102
6.4.2 ETCS无线通信系统膜计算模型建立 103
6.4.3 仿真分析 105
本章小结 108
第7章 车站进路联锁控制逻辑的形式化研究 109
7.1 联锁的安全规范 109
7.1.1 进路控制安全规范 111
7.1.2 信号控制安全规范 116
7.1.3 道岔控制安全规范 118
7.2 基于Event-B的联锁安全规范的描述和验证 118
7.2.1 联锁规范形式化描述及精化策略 118
7.2.2 车站进路联锁逻辑的Event-B初始模型 122
7.2.3 车站进路控制的Event-B建模分析 125
7.2.4 车站进路联锁控制的Event-B模型精化 127
7.2.5 车站进路联锁Event-B验证 129
7.3 基于MAS和Event-B的分布式联锁安全的描述 132
7.3.1 联锁系统MAS结构 132
7.3.2 Multi-Agent联锁层的安全规范描述 133
7.3.3 Event-B的模型规范 134
7.3.4 精化 136
本章小结 137
第8章 列车安全距离控制形式化建模与验证 138
8.1 列车自动防护原理 139
8.1.1 列车自动防护系统的基本概念 139
8.1.2 列车自动防护系统的分类 139
8.2 多列车安全距离控制模型 140
8.3 Event-B描述的列车安全距离模型 141
8.4 模型的验证 143
8.4.1 MTCS 0引入反应阶段 143
8.4.2 MTCS 1细化反应阶段 144
8.4.3 MTCS 2实现反应阶段 145
8.4.4 MTCS 3引入决策阶段 146
8.4.5 MTCS 4实现决策法则 147
本章小结 148
第9章 高可信无线通信下平直线路多列车追踪特性研究 149
9.1 平直线路列车追踪运行交通流仿真 150
9.1.1 平直线路下列车追踪MAS交通流模型结构 150
9.1.2 列车追踪运行MAS形式化定义 151
9.1.3 数值仿真与模拟 153
9.2 列车追踪交通流能耗分析 157
9.2.1 铁路能耗基本构成 157
9.2.2 单列车受力与能耗构成 157
9.2.3 快照系统概念及定义 160
9.2.4 模型建立 162
9.2.5 数值模拟与仿真分析 165
本章小结 166
第10章 线路弯道环境下多列车追踪交通流特性形式化建模 167
10.1 元胞自动机理论基础 168
10.1.1 自动机简介 168
10.1.2 元胞自动机的定义 169
10.1.3 元胞自动机的构成 170
10.1.4 元胞自动机的特征 173
10.1.5 经典元胞自动机模型 174
10.2 弯道线路模型 178
10.3 线路弯道安全速度 178
10.4 模型建立 180
10.4.1 模型结构 182
10.4.2 演化规则 183
10.5 数值模拟与仿真分析 185
10.5.1 线路曲线半径对交通流的影响 185
10.5.2 线路曲线外轨超高对交通流的影响 189
10.5.3 线路弯道长度对交通流的影响 190
本章小结 191
第11章 列控系统等级转换运营场景形式化研究 192
11.1 CTCS-3级列控系统运营场景 192
11.2 列控系统等级转换场景 193
11.2.1 地面设备 194
11.2.2 列控系统等级转换过程 195
11.3 基于MAS的场景分析 196
11.3.1 列控系统等级转换场景MAS抽象模型 196
11.3.2 车-地主体Agent设计 197
11.4 列控系统等级转换运营场景CPN建模 199
11.4.1 场景顶层模型设计 199
11.4.2 列车Agent内部模型设计 201
11.4.3 RBC Agent内部模型设计 210
11.5 仿真分析 217
本章小结 219
第12章 列控系统降级场景建模与仿真 220
12.1 正常运行时列控系统降级情况的建模与仿真 220
12.1.1 正常运行时列控系统降级场景介绍 221
12.1.2 正常运行时列控系统降级情况场景的建模 222
12.1.3 正常运行时列控系统降级情况场景仿真分析 225
12.2 车载设备故障导致降级运行建模与仿真 227
12.2.1 车载设备故障导致降级场景的介绍 227
12.2.2 控车设备故障分析 228
12.2.3 车载设备故障导致降级场景分析 228
12.2.4 车载设备故障导致降级模型设计 229
12.2.5 仿真分析 231
12.3 应答器故障导致降级列控系统的建模与仿真 234
12.3.1 应答器故障导致列控系统降级场景介绍 234
12.3.2 应答器故障因素分析 234
12.3.3 应答器故障导致的等级转换场景分析 234
12.3.4 应答设备故障降级模型设计 236
12.3.5 仿真分析 238
本章小结 240
附录A IEC 61508安全标准介绍 242
附录B 高速铁路设计术语和符号 247
附录C《铁路技术管理规程》（高速铁路部分）有关线路、桥梁及隧道部分摘录 252
附录D《铁路技术管理规程》（高速铁路部分）有关车站及枢纽部分摘录 257
参考文献 259