列車運行控制系統規範建模與驗證

內容豐富，注重背景，可以作為研究生、教師以及軌道交通控制領域相關的科研人員瞭解列控系統規範的建模與驗證的基本思想和方法的參考書，主要介紹了實現列控系統需求規範的嚴格建模與驗證所必須的理論、方法和關鍵技術，內容包括現代列車運行控制系統的特點和相關標準規範、系統規範的嚴格建模與驗證體系、模型檢驗相關基礎知識、需求規範的管理和追蹤、列控領域的UML建模以及針對CTCS－3系統規範展開的實例分析。 ^[1] 

本書主要介紹了實現列控系統需求規範的嚴格建模與驗證所必須的理論、方法和關鍵技術，內容包括現代列車運行控制系統的特點和相關標準規範、系統規範的嚴格建模與驗證體系、模型檢驗相關基礎知識、需求規範的管理和追蹤、列控領域的UML建模以及針對CTCS－3系統規範展開的實例分析。

本書內容豐富，注重背景，可以作為研究生、教師以及軌道交通控制領域相關的科研人員瞭解列控系統規範的建模與驗證的基本思想和方法的參考書。

第一章　概 述

第一節　軌道交通列控系統發展趨勢

第二節　列控系統規範驗證的意義

第三節　列控系統規範的建模驗證方法

第四節　列控系統規範的嚴格建模與驗證體系

本章參考文獻

第二章 系統需求規範建模與驗證基礎

第一節　系統需求規範

第二節　驗證和確認的概念

第三節　系統開發模型

第四節　UML基礎知識

第五節　符號模型檢驗

本章參考文獻

第三章 列控系統的需求規範驗證內容與體系

第一節　列控系統需求規範驗證內容

第二節　列控系統需求規範驗證方法體系

第三節　列控系統需求規範驗證流程

本章參考文獻

第四章　需求規範的管理

第一節　需求規範管理的概念與意義

第二節　需求規範管理的任務

第三節　需求規範管理流程

本章參考文獻

第五章　列控系統的UML建模

第一節　列控系統UML模型庫

第二節　列控系統規範的UML模型

本章參考文獻

第六章　列控系統的形式化驗證

第一節　列控系統規範UML模型到NuSMV的轉換

第二節　列控系統模型的約簡

第三節　列控系統規範驗證結果分析

本章參考文獻

第七章　實例分析

第一節　背景介紹

第二節　需求規範管理

第三節　CTCS一3級系統需求規範的UML建模

第四節　NuSMV轉換

第五節　驗證結果分析

本章參考文獻

附錄A　NuSMV系統簡介

附錄B　系統開發模型介紹