列车运行安全行为建模与形式化技术研究

第1章 绪论
1．1 列车运行安全背景及意义
1．2 基于无线通信的列车运行控制系统
1．2．1 列车运行控制系统构成与分类
1．2．2 CTCS列控系统
1．2．3 GSM-R铁路无线通信系统
1．3 列车控制形式化研究现状
1．4 本书内容与结构安排
第2章 形式化建模理论与复杂系统理论
2．1 建模基本理论
2．1．1 系统、模型、仿真的基本概念
2．1．2 系统模型的分类
2．1．3 建模方法的分类
2．1．4 建模的一般原则
2．1．5 建模步骤的划分
2．2 形式化理论
2．2．1 形式化概念
2．2．2 形式化分类
2．2．3 形式化验证方法
2．2．4 常见的形式化建模方法
2．3 复杂系统建模理论
2．3．1 复杂系统
2．3．2 复杂适应系统理论
2．3．3 分布式人工智能
2．3．4 多智能体基础理论
2．4 Event-B方法及Rodin平台
2．4．1 Event-B基本结构
2．4．2 Event-B数学体系
2．4．3 Event-B模型精化和证明义务
2．4．4 RODIN平台
本章小结
第3章 交通系统建模
3．1 交通系统仿真
3．1．1 交通系统仿真基本概念
3．1．2 系统分类与系统模型
3．2 交通流理论
3．2．1 交通流理论分类
3．2．2 交通流理论参数
3．2．3 交通流主要研究内容
3．3 交通多分辨率建模方法
3．3．1 宏观交通建模仿真
3．3．2 微观交通建模仿真
3．3．3 中观交通建模仿真
本章小结
第4章 CTCS-4级车地通信机制的形式化研究
4．1 通信顺序进程形式化理论基础
4．1．1 通信与递归
4．1．2 CSP的运算符
4．1．3 过程行为
4．1．4 进程的迹
4．1．5 CSP模型检测工具
4．1．6 故障发散检测器FDR
4．2 基于MAs的RBC切换场景描述及车地通信信息交互流的实现
4．2．1 列控系统多Agent系统抽象
4．2．2 基于CPN的混合Agent模型
4．2．3 MAS模型形式化定义
4．2．4 基于CORBA的发布订阅模式的车地通信
4．3 基于CSP的车地实时通信协议形式化建模与验证
4．3．1 MAS系统通信协议形式化验证框架
4．3．2 列控系统实时通信协议的形式化建模
4．3．3 CSP语言对车地实时通信协议建模
4．3．4 Casper+FDR对实时通信协议验证
4．4 注入故障的Agent~黾信模型
4．4．1 故障导向安全性功能分析与验证
4．4．2 列控系统消息处理实时性分析
4．4．3 通信时效性分析
本章小结
第5章 基于SPN的高可信无线通信形式化建模与分斩
第6章 基于细胞膜计算的无线通信并行形式化建模
第7章 车站进路联锁控制逻辑的形式化研究
第8章 列车安全距离控制形式化建模与验证
第9章 高可信无线通信下平直线路多列车追踪特性研究
第10章 线路弯道环境下多列车追踪交通流特性形式化建模
第11章 列控系统等级转换运营场景形式化研究
第12章 列控系统降级场景建模与仿真
附录A IEC61508安全标准介绍
附录B 高速铁路设计术语和符号
附录C 《铁路技术管理规程》（高速铁路部分）有关线路、桥架及隧道部分摘录
附录D 《铁路技术管理规程》（高速铁路部分）有关车站及枢纽部分摘录
参考文献