列車運(yùn)行控制系統(tǒng)實(shí)時(shí)性的建模與驗(yàn)證

第1章 列車運(yùn)行控制系統(tǒng)實(shí)時(shí)性概述
1．1 列車運(yùn)行控制系統(tǒng)簡(jiǎn)介
1．1．1 列車運(yùn)行控制系統(tǒng)的現(xiàn)狀與發(fā)展
1．1．2 列車運(yùn)行控制系統(tǒng)的組成
1．1．3 列車運(yùn)行控制系統(tǒng)的特點(diǎn)
1．2 列車運(yùn)行控制系統(tǒng)的實(shí)時(shí)性要求
1．3 國(guó)內(nèi)外研究現(xiàn)狀
1．4 列車運(yùn)行控制系統(tǒng)實(shí)時(shí)性的建模與驗(yàn)證方法
第2章 基于UML的列控系統(tǒng)實(shí)時(shí)性研究
2．1 UML概述
2．1．1 UML的定義
2．1．2 UML的組成
2．1．3 UML建模機(jī)制
2．2 UML擴(kuò)展機(jī)制
2．2．1 約束
2．2．2 標(biāo)記值
2．2．3 構(gòu)造型
2．3 列控系統(tǒng)的UML模型
2．3．1 用例圖
2．3．2 類圖
2．3．3 活動(dòng)圖
2．3．4 部署圖
2．3．5 序列圖
2．3．6 狀態(tài)圖
2．4 基于UML的模型轉(zhuǎn)換方法
2．4．1 模型轉(zhuǎn)換的概念
2．4．2 UML元模型
第3章 基于UML與CSP的實(shí)時(shí)系統(tǒng)建模與分析
3．1 CSP相關(guān)理論
3．1．1 CSP的語(yǔ)法和語(yǔ)義
3．1．2 CSP的實(shí)時(shí)性擴(kuò)展
3．2 UML到CSP的轉(zhuǎn)換規(guī)則
3．2．1 活動(dòng)圖轉(zhuǎn)換規(guī)則
3．2．2 狀態(tài)圖轉(zhuǎn)換規(guī)則
3．3 模型轉(zhuǎn)換中特性的保持與轉(zhuǎn)換規(guī)則的證明
3．3．1 模型轉(zhuǎn)換中特性的保持
3．3．2 模型轉(zhuǎn)換規(guī)則的證明
3．4 UML轉(zhuǎn)換至CSP的列控系統(tǒng)實(shí)時(shí)性分析實(shí)例
第4章 基于時(shí)間自動(dòng)機(jī)的系統(tǒng)建模與驗(yàn)證
4．1 時(shí)間自動(dòng)機(jī)
4．1．1 時(shí)間約束和時(shí)間解釋
4．1．2 時(shí)間語(yǔ)言
4．1．3 時(shí)間自動(dòng)機(jī)的語(yǔ)義
4．1．4 時(shí)間自動(dòng)機(jī)的積
4．2 基于時(shí)間自動(dòng)機(jī)的形式化建模
4．3 模型檢驗(yàn)方法驗(yàn)證實(shí)時(shí)系統(tǒng)
4．3．1 時(shí)序邏輯
4．3．2 時(shí)序邏輯的時(shí)間化
4．3．3 驗(yàn)證流程
4．4 定理證明方法驗(yàn)證實(shí)時(shí)系統(tǒng)
……