列車運(yùn)行控制系統(tǒng)規(guī)范建模與驗(yàn)證

前言

　　軌道交通具有運(yùn)能大、能耗低、污染小、安全舒適等優(yōu)勢(shì)，是最具可持續(xù)性和環(huán)境友好性的交通運(yùn)輸系統(tǒng)，在我國(guó)綜合交通體系中具有不可替代的突出地位。作為一種大容量公共交通王具，軌道交通系統(tǒng)的安全性直接關(guān)系到廣大乘客的生命財(cái)產(chǎn)安全，必須采用高性能的列車運(yùn)行控制系統(tǒng)（簡(jiǎn)稱列控系統(tǒng)）保證列車安全、正點(diǎn)、快捷、舒適、高密度不間斷運(yùn)行。隨著科學(xué)技術(shù)的飛速發(fā)展，計(jì)算機(jī)技術(shù)、通信技術(shù)已經(jīng)廣泛地應(yīng)用于軌道交通，列控系統(tǒng)已發(fā)展成為以安全計(jì)算機(jī)為核心的覆蓋軌道交通全線所有站點(diǎn)、所有列車的網(wǎng)絡(luò)化復(fù)雜控制系統(tǒng)——自動(dòng)列車運(yùn)行控制系統(tǒng)。

內(nèi)容概要

本書主要介紹了實(shí)現(xiàn)列控系統(tǒng)需求規(guī)范的嚴(yán)格建模與驗(yàn)證所必須的理論、方法和關(guān)鍵技術(shù)，內(nèi)容包括現(xiàn)代列車運(yùn)行控制系統(tǒng)的特點(diǎn)和相關(guān)標(biāo)準(zhǔn)規(guī)范、系統(tǒng)規(guī)范的嚴(yán)格建模與驗(yàn)證體系、模型檢驗(yàn)相關(guān)基礎(chǔ)知識(shí)、需求規(guī)范的管理和追蹤、列控領(lǐng)域的UML建模以及針對(duì)CTCS－3系統(tǒng)規(guī)范展開的實(shí)例分析。    本書內(nèi)容豐富，注重背景，可以作為研究生、教師以及軌道交通控制領(lǐng)域相關(guān)的科研人員了解列控系統(tǒng)規(guī)范的建模與驗(yàn)證的基本思想和方法的參考書。

書籍目錄

第一章　概  述　第一節(jié)　軌道交通列控系統(tǒng)發(fā)展趨勢(shì)　第二節(jié)　列控系統(tǒng)規(guī)范驗(yàn)證的意義　第三節(jié)　列控系統(tǒng)規(guī)范的建模驗(yàn)證方法　第四節(jié)　列控系統(tǒng)規(guī)范的嚴(yán)格建模與驗(yàn)證體系　本章參考文獻(xiàn)第二章  系統(tǒng)需求規(guī)范建模與驗(yàn)證基礎(chǔ)  第一節(jié)　系統(tǒng)需求規(guī)范  第二節(jié)　驗(yàn)證和確認(rèn)的概念  第三節(jié)　系統(tǒng)開發(fā)模型  第四節(jié)　UML基礎(chǔ)知識(shí)  第五節(jié)　符號(hào)模型檢驗(yàn)  本章參考文獻(xiàn)第三章  列控系統(tǒng)的需求規(guī)范驗(yàn)證內(nèi)容與體系　第一節(jié)　列控系統(tǒng)需求規(guī)范驗(yàn)證內(nèi)容　第二節(jié)　列控系統(tǒng)需求規(guī)范驗(yàn)證方法體系　第三節(jié)　列控系統(tǒng)需求規(guī)范驗(yàn)證流程　本章參考文獻(xiàn)第四章　需求規(guī)范的管理　第一節(jié)　需求規(guī)范管理的概念與意義　第二節(jié)　需求規(guī)范管理的任務(wù)　第三節(jié)　需求規(guī)范管理流程　本章參考文獻(xiàn)第五章　列控系統(tǒng)的UML建模　第一節(jié)　列控系統(tǒng)UML模型庫(kù)　第二節(jié)　列控系統(tǒng)規(guī)范的UML模型　本章參考文獻(xiàn)第六章　列控系統(tǒng)的形式化驗(yàn)證　第一節(jié)　列控系統(tǒng)規(guī)范UML模型到NuSMV的轉(zhuǎn)換　第二節(jié)　列控系統(tǒng)模型的約簡(jiǎn)　第三節(jié)　列控系統(tǒng)規(guī)范驗(yàn)證結(jié)果分析　本章參考文獻(xiàn)第七章　實(shí)例分析  第一節(jié)　背景介紹  第二節(jié)　需求規(guī)范管理  第三節(jié)　CTCS一3級(jí)系統(tǒng)需求規(guī)范的UML建模  第四節(jié)　NuSMV轉(zhuǎn)換  第五節(jié)　驗(yàn)證結(jié)果分析  本章參考文獻(xiàn)附錄A　NuSMV系統(tǒng)簡(jiǎn)介附錄B　系統(tǒng)開發(fā)模型介紹

章節(jié)摘錄

　?。?）屬性　　一個(gè)類可以有一個(gè)或多個(gè)屬性，或者沒有屬性。屬性用來(lái)描述該類的對(duì)象所具有的靜態(tài)特征。類的屬性分為兩類：一類屬性代表的狀態(tài)可以被其他對(duì)象存取；另一類屬性代表的是對(duì)象的內(nèi)部狀態(tài)，它們只能夠被類的操作所存取。屬性必須命名，以區(qū)別類的其他屬性。當(dāng)一個(gè)類的屬性被完整地定義后，它的任何一個(gè)對(duì)象的狀態(tài)都被這些屬性的特定取值所決定。在需求分析階段，只抽取那些系統(tǒng)中需要使用的特征作為類的屬性?！　≌缱兞坑蓄愋鸵粯樱瑢傩砸彩怯蓄愋偷?，屬性的類型反映屬性的種類。比如，屬性的類型可以是整型、實(shí)型、布爾型、枚

圖書封面

評(píng)論、評(píng)分、閱讀與下載

---

    列車運(yùn)行控制系統(tǒng)規(guī)范建模與驗(yàn)證 PDF格式下載

---