列車運行安全行為建模與形式化技術(shù)研究

第1章 緒論
1．1 列車運行安全背景及意義
1．2 基于無線通信的列車運行控制系統(tǒng)
1．2．1 列車運行控制系統(tǒng)構(gòu)成與分類
1．2．2 CTCS列控系統(tǒng)
1．2．3 GSM-R鐵路無線通信系統(tǒng)
1．3 列車控制形式化研究現(xiàn)狀
1．4 本書內(nèi)容與結(jié)構(gòu)安排
第2章 形式化建模理論與復(fù)雜系統(tǒng)理論
2．1 建?；纠碚?br />2．1．1 系統(tǒng)、模型、仿真的基本概念
2．1．2 系統(tǒng)模型的分類
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 復(fù)雜系統(tǒng)建模理論
2．3．1 復(fù)雜系統(tǒng)
2．3．2 復(fù)雜適應(yīng)系統(tǒng)理論
2．3．3 分布式人工智能
2．3．4 多智能體基礎(chǔ)理論
2．4 Event-B方法及Rodin平臺
2．4．1 Event-B基本結(jié)構(gòu)
2．4．2 Event-B數(shù)學(xué)體系
2．4．3 Event-B模型精化和證明義務(wù)
2．4．4 RODIN平臺
本章小結(jié)
第3章 交通系統(tǒng)建模
3．1 交通系統(tǒng)仿真
3．1．1 交通系統(tǒng)仿真基本概念
3．1．2 系統(tǒng)分類與系統(tǒng)模型
3．2 交通流理論
3．2．1 交通流理論分類
3．2．2 交通流理論參數(shù)
3．2．3 交通流主要研究內(nèi)容
3．3 交通多分辨率建模方法
3．3．1 宏觀交通建模仿真
3．3．2 微觀交通建模仿真
3．3．3 中觀交通建模仿真
本章小結(jié)
第4章 CTCS-4級車地通信機(jī)制的形式化研究
4．1 通信順序進(jìn)程形式化理論基礎(chǔ)
4．1．1 通信與遞歸
4．1．2 CSP的運算符
4．1．3 過程行為
4．1．4 進(jìn)程的跡
4．1．5 CSP模型檢測工具
4．1．6 故障發(fā)散檢測器FDR
4．2 基于MAs的RBC切換場景描述及車地通信信息交互流的實現(xiàn)
4．2．1 列控系統(tǒng)多Agent系統(tǒng)抽象
4．2．2 基于CPN的混合Agent模型
4．2．3 MAS模型形式化定義
4．2．4 基于CORBA的發(fā)布訂閱模式的車地通信
4．3 基于CSP的車地實時通信協(xié)議形式化建模與驗證
4．3．1 MAS系統(tǒng)通信協(xié)議形式化驗證框架
4．3．2 列控系統(tǒng)實時通信協(xié)議的形式化建模
4．3．3 CSP語言對車地實時通信協(xié)議建模
4．3．4 Casper+FDR對實時通信協(xié)議驗證
4．4 注入故障的Agent~黽信模型
4．4．1 故障導(dǎo)向安全性功能分析與驗證
4．4．2 列控系統(tǒng)消息處理實時性分析
4．4．3 通信時效性分析
本章小結(jié)
第5章 基于SPN的高可信無線通信形式化建模與分?jǐn)?br />第6章 基于細(xì)胞膜計算的無線通信并行形式化建模
第7章 車站進(jìn)路聯(lián)鎖控制邏輯的形式化研究
第8章 列車安全距離控制形式化建模與驗證
第9章 高可信無線通信下平直線路多列車追蹤特性研究
第10章 線路彎道環(huán)境下多列車追蹤交通流特性形式化建模
第11章 列控系統(tǒng)等級轉(zhuǎn)換運營場景形式化研究
第12章 列控系統(tǒng)降級場景建模與仿真
附錄A IEC61508安全標(biāo)準(zhǔn)介紹
附錄B 高速鐵路設(shè)計術(shù)語和符號
附錄C 《鐵路技術(shù)管理規(guī)程》（高速鐵路部分）有關(guān)線路、橋架及隧道部分摘錄
附錄D 《鐵路技術(shù)管理規(guī)程》（高速鐵路部分）有關(guān)車站及樞紐部分摘錄
參考文獻(xiàn)