123,123,123

內(nèi)容簡(jiǎn)介

　　《列車(chē)運(yùn)行控制系統(tǒng)實(shí)時(shí)性的建模與驗(yàn)證》系統(tǒng)地介紹了列車(chē)運(yùn)行控制系統(tǒng)實(shí)時(shí)性的特點(diǎn)，以及建模與驗(yàn)證方法。重點(diǎn)闡述了基于UML、CSP、時(shí)間自動(dòng)機(jī)、著色Petri網(wǎng)、馬爾可夫鏈等理論和方法的列控系統(tǒng)，探討了實(shí)現(xiàn)列控系統(tǒng)實(shí)時(shí)陛建模與驗(yàn)證所必須的理論與關(guān)鍵技術(shù)。在應(yīng)用方面，介紹了支持相關(guān)研究方法的技術(shù)手段及其算法?！读熊?chē)運(yùn)行控制系統(tǒng)實(shí)時(shí)性的建模與驗(yàn)證》適合作為高等院校鐵路信號(hào)及相關(guān)專(zhuān)業(yè)的教學(xué)參考用書(shū)，也可供相關(guān)領(lǐng)域研究人員參考。

作者簡(jiǎn)介

　　謝雨飛，男，任教于北京建筑大學(xué)電氣與信息工程學(xué)院。主要研究方向：復(fù)雜系統(tǒng)建模與求解、網(wǎng)絡(luò)安全技術(shù)等，主持國(guó)家自然基金項(xiàng)目1項(xiàng)，發(fā)表EI、核心期刊論文10余篇。

圖書(shū)目錄

第1章列車(chē)運(yùn)行控制系統(tǒng)實(shí)時(shí)性概述
1．1 列車(chē)運(yùn)行控制系統(tǒng)簡(jiǎn)介
1．1．1 列車(chē)運(yùn)行控制系統(tǒng)的現(xiàn)狀與發(fā)展
1．1．2 列車(chē)運(yùn)行控制系統(tǒng)的組成
1．1．3 列車(chē)運(yùn)行控制系統(tǒng)的特點(diǎn)
1．2 列車(chē)運(yùn)行控制系統(tǒng)的實(shí)時(shí)性要求
1．3 國(guó)內(nèi)外研究現(xiàn)狀
1．4 列車(chē)運(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 類(lèi)圖
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)
……