列车运行安全行为建模与形式化技术研究PDF|Epub|txt|kindle电子书版本网盘下载

列车运行安全行为建模与形式化技术研究PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第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 故障发散检测器FDR50

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 软件仿真工具TimeNET88

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