基于SCADE的CBTC區(qū)域控制器軟件開發(fā).pdf

1、區(qū)域控制器(Zone Controller-ZC)是基于通信列車運(yùn)行控制系統(tǒng)(Communications Based Train Control system-CBTC)系統(tǒng)的地面控制核心設(shè)備,負(fù)責(zé)列車移動(dòng)授權(quán)的計(jì)算和運(yùn)行安全保障。ZC是一個(gè)復(fù)雜龐大的安全關(guān)鍵系統(tǒng),其軟件開發(fā)在規(guī)范刻畫、設(shè)計(jì)、驗(yàn)證等諸多方面面臨挑戰(zhàn)。近年來(lái),基于模型的軟件開發(fā)方法在安全關(guān)鍵領(lǐng)域逐漸被認(rèn)可,本文研究基于SCADE模型的ZC軟件開發(fā)方法,主要工作體現(xiàn)在如下

2、方面:
　　 (1)以軌道交通控制系統(tǒng)為背景,研究了安全關(guān)鍵性系統(tǒng)的相關(guān)安全標(biāo)準(zhǔn),分析了模型驅(qū)動(dòng)開發(fā)的優(yōu)勢(shì),并介紹了SCADE模型開發(fā)工具。
　　 (2)研究了SCADE理論基礎(chǔ)—同步編程理論。研究了LUSTRE語(yǔ)言的語(yǔ)法規(guī)則和UJSTRE語(yǔ)言對(duì)反應(yīng)式系統(tǒng)的進(jìn)行模型描述的抽象方法。分析了數(shù)據(jù)流圖和安全狀態(tài)機(jī)這兩種形式化建模機(jī)制的語(yǔ)義基礎(chǔ)、建模方法以及模型的特性。研究了同步編程理論對(duì)模型的兩種確認(rèn)方法模擬仿真和形式化驗(yàn)證。

3、
　　 (3)采用SCADE模型工具,對(duì)ZC進(jìn)行建模。對(duì)ZC進(jìn)行了形式化描述,建立ZC的SCADE總體模型。通過(guò)分析區(qū)域控制器控制列車的典型場(chǎng)景,將ZC的主要功能劃分為列車管理功能、進(jìn)路匹配功能和MA計(jì)算功能,詳細(xì)的設(shè)計(jì)了各功能的軟件流程。采用安全自動(dòng)機(jī)建模機(jī)制,建立了列車管理功能的模型;采用數(shù)據(jù)流建模機(jī)制,建立了進(jìn)路匹配功能和MA計(jì)算功能的模型。
　　 (4)采用SCADE仿真與驗(yàn)證工具,對(duì)ZC模型進(jìn)行檢驗(yàn)。采用故障模