基于SCADE的地鐵列車測速定位系統(tǒng)建模與安全性分析.pdf

1、測速定位系統(tǒng)是城市軌道交通列車運行控制系統(tǒng)車載設(shè)備的關(guān)鍵子系統(tǒng)，它實時檢測列車速度與當前位置，所測數(shù)據(jù)將用于列車移動授權(quán)的計算，測速定位系統(tǒng)的精確性和可靠性直接影響著行車安全和效率?；谀Ｐ偷能浖_發(fā)方法如今在安全關(guān)鍵領(lǐng)域逐漸被認可，高安全性應(yīng)用開發(fā)環(huán)境(Safety critical application developmentenvironment，SCADE)，為安全苛求系統(tǒng)、軟件研發(fā)人員提供認證級解決方案，其基于模型的開發(fā)方式

2、、內(nèi)置仿真器與模型驗證工具Design Verifier保證了所開發(fā)系統(tǒng)的功能性及安全性。本文基于SCADE對測速定位系統(tǒng)進行建模、仿真、驗證及安全性分析。
　　本文主要工作有:
　　1、以地鐵列車運行控制系統(tǒng)為背景，研究了安全關(guān)鍵性系統(tǒng)的開發(fā)方式，分析了基于模型開發(fā)方式的優(yōu)點，詳細介紹了SCADE高安全性應(yīng)用開發(fā)環(huán)境。
　　2、根據(jù)地鐵列車測速定位系統(tǒng)的功能特點，將測速定位系統(tǒng)劃分為輪徑校正、列車位置初始化、列車位置

3、確定和列車定位失效管理4個子系統(tǒng)，并詳細分析了這些子系統(tǒng)的流程，設(shè)計了各個子系統(tǒng)的建模方法。
　　3、為了提高列車測速定位系統(tǒng)設(shè)計的安全性，依據(jù)軌道交通1474.3規(guī)范，基于形式化模型驅(qū)動開發(fā)理論，使用高安全性應(yīng)用開發(fā)環(huán)境(SCADE)的數(shù)據(jù)流圖和安全狀態(tài)機建模機制對測速定位系統(tǒng)的各個子系統(tǒng)建立模型，通過各子系統(tǒng)接口整合各子系統(tǒng)模型，最終得到完整的測速定位系統(tǒng)模型。
　　4、依據(jù)模型內(nèi)置的邏輯運算公式和模型運行中產(chǎn)生的中間數(shù)

4、據(jù)，使用SCADE的仿真與驗證工具，通過驗證邏輯運算結(jié)果，達到檢驗?zāi)Ｐ凸δ芎桶踩缘哪康?。通過驗證證明所設(shè)計模型滿足系統(tǒng)功能性和安全性需求。
　　5、在使用SCADE驗證了模型整體安全性的基礎(chǔ)上，基于DeductiveCause-Consequence Analysis(DCCA)方法嚴厲的邏輯框架，分析了導(dǎo)致測速定位系統(tǒng)危害的失效模式，使用SCADE驗證機制尋找出了導(dǎo)致測速定位系統(tǒng)危害的最小關(guān)鍵集，為高安全性系統(tǒng)的設(shè)計提供依據(jù)。