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

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