高雪娟, 陳啟香, 鄭鴻昌

(1.株洲中車時(shí)代電氣股份有限公司 通信信號(hào)事業(yè)部，湖南 株洲 412001;2.寶雞文理學(xué)院 電子電氣工程學(xué)院，陜西 寶雞 721000)

應(yīng)用ETDFA生成CBTC聯(lián)鎖軟件形式化模型的方法

高雪娟1, 陳啟香2, 鄭鴻昌1

(1.株洲中車時(shí)代電氣股份有限公司 通信信號(hào)事業(yè)部，湖南 株洲 412001;2.寶雞文理學(xué)院 電子電氣工程學(xué)院，陜西 寶雞 721000)

CBTC系統(tǒng)的聯(lián)鎖軟件為SIL4級(jí)的高安全、高可靠軟件，目前廣泛使用的軟件測(cè)試和仿真驗(yàn)證的結(jié)果嚴(yán)重依賴選取的測(cè)試向量，要保證高覆蓋率的測(cè)試十分困難;EN50128中強(qiáng)烈推薦SIL4等級(jí)的軟件使用形式化方法完成軟件需求規(guī)格說明書和軟件設(shè)計(jì)，因此，采用形式化的方法設(shè)計(jì)軟件，是構(gòu)造高可靠、高安全軟件的一個(gè)重要途徑;總結(jié)了現(xiàn)有的CBTC系統(tǒng)中聯(lián)鎖子系統(tǒng)集成方式及優(yōu)缺點(diǎn)，并使用事件確定有限自動(dòng)機(jī)ETDFA(event deterministic finite automata)模型對(duì)適用性更優(yōu)的升級(jí)型集成方式的聯(lián)鎖軟件的聯(lián)鎖邏輯完成形式化定義，保證聯(lián)鎖邏輯的正確性，減少軟件的不確定性描述;以辦理進(jìn)路為例生成聯(lián)鎖對(duì)象的ETDFA模型，驗(yàn)證該方法的有效性和可行性;該方法不僅為CBTC聯(lián)鎖軟件的設(shè)計(jì)與開發(fā)提供新思路，而且有助于安全苛求軟件的形式化驗(yàn)證與分析，提高聯(lián)鎖軟件的安全性和正確性。

CBTC；聯(lián)鎖軟件；ETDFA；形式化方法

0 引言

CBTC(communication based train control,基于通信的列車控制)系統(tǒng)中的聯(lián)鎖軟件需支持CBTC模式和后備模式下列車的運(yùn)行防護(hù)，同時(shí)能滿足混線跑的需求，因此，傳統(tǒng)的聯(lián)鎖軟件并不能滿足CBTC的更小追蹤間隔、更高運(yùn)輸效率的要求。作為安全完整性等級(jí)為SIL4[1]級(jí)的軟件，對(duì)CBTC聯(lián)鎖軟件的安全性、可靠性都有較高的要求。目前對(duì)聯(lián)鎖軟件安全性的確認(rèn)，主要通過模擬驗(yàn)證和仿真測(cè)試，如文獻(xiàn)[2]研究了計(jì)算機(jī)聯(lián)鎖軟件測(cè)試的安全性評(píng)價(jià)準(zhǔn)則，文獻(xiàn)[3]通過EVALPSN軟件模擬驗(yàn)證聯(lián)鎖系統(tǒng)的安全性，文獻(xiàn)[4]對(duì)聯(lián)鎖系統(tǒng)的UML模型用Rhapsody模擬分析其安全性。但軟件測(cè)試和仿真驗(yàn)證的結(jié)果嚴(yán)重依賴選取的測(cè)試向量，要保證高覆蓋率的測(cè)試十分困難。

EN50128[5]中強(qiáng)烈推薦SIL4等級(jí)的軟件使用形式化方法完成軟件需求規(guī)格說明書和軟件設(shè)計(jì)。采用形式化的方法設(shè)計(jì)軟件，是構(gòu)造高可靠、高安全軟件的一個(gè)重要途徑。統(tǒng)一建模語言UML(unified modelling language)的順序圖能描述對(duì)象間傳遞的消息及時(shí)間順序，但由于UML是半形式化語言，需將系統(tǒng)的順序圖用形式化方法完成描述及驗(yàn)證。

文獻(xiàn)[6-7]分別基于B方法和Z語言將UML模型進(jìn)行形式化描述，但用這兩種方法生成的形式化模型對(duì)于對(duì)詳見的交互路徑存在表達(dá)模糊的問題；文獻(xiàn)[8]使用抽象狀態(tài)機(jī)ASM(abstract state machine)實(shí)現(xiàn)對(duì)序列圖語義的建模，但對(duì)于復(fù)雜的UML2.0的序列圖，該方法生成的模型由于缺乏精確的定義給驗(yàn)證造成了困難；文獻(xiàn)[9]以XYZ/E的線性時(shí)序邏輯為基礎(chǔ)完成序列圖的形式化描述；文獻(xiàn)[10]利用進(jìn)程代數(shù)表達(dá)式映射序列圖中的交互消息及執(zhí)行順序，但缺少直觀性；文獻(xiàn)[11]使用Promela語言描述序列圖，但所生成的代碼不利于從模型中生成測(cè)試用例；文獻(xiàn)[12-13]使用Petri網(wǎng)對(duì)序列圖進(jìn)行形式化描述，但其表達(dá)的屬性的可判定性依賴其屬性[14]；文獻(xiàn)[15-19]使用自動(dòng)機(jī)形式化描述序列圖，但對(duì)序列圖中每個(gè)對(duì)象狀態(tài)的遷移、對(duì)象之間的交互描述的不夠清楚。

本文針對(duì)序列圖中的對(duì)象之間的交互，采用基于事件確定有限自動(dòng)機(jī)ETDFA描述UML2.0序列圖，并完成CBTC聯(lián)鎖軟件的形式化模型生成，驗(yàn)證方法的有效性和可用性。

1 CBTC聯(lián)鎖軟件

1.1 聯(lián)鎖集成方式

目前CBTC系統(tǒng)中的聯(lián)鎖集成方式分為兼容型集成方式的聯(lián)鎖和升級(jí)型集成方式的聯(lián)鎖[20]，表1為兩種聯(lián)鎖集成方式的對(duì)比。

表1 不同集成方式的CBTC聯(lián)鎖系統(tǒng)對(duì)比

圖1為以兼容型方式集成聯(lián)鎖的結(jié)構(gòu)框圖，圖2為以升級(jí)型方式集成聯(lián)鎖的結(jié)構(gòu)框圖。

本文基于升級(jí)型集成方式的聯(lián)鎖實(shí)現(xiàn)CBTC聯(lián)鎖系統(tǒng)的ETDFA模型。

圖1 兼容型集成聯(lián)鎖框圖

圖2 升級(jí)型集成聯(lián)鎖框圖

1.2 CBTC聯(lián)鎖系統(tǒng)功能

圖3為升級(jí)型集成方式的聯(lián)鎖系統(tǒng)結(jié)構(gòu)圖。

圖3 升級(jí)型集成方式聯(lián)鎖系統(tǒng)結(jié)構(gòu)圖

CBTC聯(lián)鎖系統(tǒng)與傳統(tǒng)聯(lián)鎖的不同主要有以下幾個(gè)方面：

1)軌道區(qū)段狀態(tài)：在CBTC模式下，由區(qū)域控制器向聯(lián)鎖提供列車位置信息；在后備模式下，通過計(jì)軸設(shè)備獲得物理區(qū)段占用情況。

2)進(jìn)路建立：為提高運(yùn)營(yíng)效率，縮短追蹤間隔，CBTC系統(tǒng)允許同時(shí)有2列及以上的列車在信號(hào)機(jī)所防護(hù)的同一條進(jìn)路中。相比大鐵聯(lián)鎖，建立進(jìn)路時(shí)，不再檢查進(jìn)路中區(qū)段是否空閑。

3)進(jìn)路解鎖：大鐵聯(lián)鎖中進(jìn)路解鎖包括三點(diǎn)檢查解鎖和取消進(jìn)路解鎖，但在CBTC系統(tǒng)下，列車追蹤間隔較密，當(dāng)前行列車還未出清信號(hào)機(jī)內(nèi)方區(qū)段時(shí)，已為后續(xù)列車再次辦理進(jìn)路，后續(xù)列車緊隨其后駛?cè)朐撨M(jìn)路，這種情況下，無法通過三點(diǎn)檢查實(shí)現(xiàn)區(qū)段解鎖。CBTC聯(lián)鎖系統(tǒng)針對(duì)這種情況有兩種解決措施：一是通過CBTC系統(tǒng)中列車通過信號(hào)機(jī)的信息來解鎖進(jìn)路；二是辦理進(jìn)路時(shí)，只有當(dāng)信號(hào)機(jī)內(nèi)方第一區(qū)段空閑時(shí)，才允許辦理后續(xù)列車的進(jìn)路[21]。

4)信號(hào)顯示：CBTC聯(lián)鎖系統(tǒng)在CBTC模式下，若信號(hào)機(jī)使用傳統(tǒng)點(diǎn)燈方式，當(dāng)信號(hào)機(jī)發(fā)生故障，對(duì)運(yùn)營(yíng)效率產(chǎn)生極大影響，而且，在CBTC模式下，信號(hào)開放不檢查進(jìn)路內(nèi)區(qū)段的空閑狀態(tài)，違背了計(jì)算機(jī)聯(lián)鎖技術(shù)條件中的規(guī)定，因此，在CBTC模式下，信號(hào)顯示采用滅燈方式，簡(jiǎn)化了系統(tǒng)的運(yùn)用條件。

5)保護(hù)進(jìn)路：類似大鐵的延續(xù)進(jìn)路，為避免列車因停車誤差而造成安全隱患，CBTC系統(tǒng)為接車進(jìn)路設(shè)置“保護(hù)進(jìn)路”，一般為進(jìn)路終端停車點(diǎn)信號(hào)機(jī)內(nèi)方一個(gè)區(qū)段。當(dāng)接車進(jìn)路建立、列車駛?cè)胗|發(fā)區(qū)段時(shí)，“保護(hù)進(jìn)路”自動(dòng)建立?！氨Ｗo(hù)進(jìn)路”的解鎖方式與大鐵延續(xù)進(jìn)路類似。

6)運(yùn)行方向：與大鐵聯(lián)鎖的區(qū)間方向電路不同，CBTC聯(lián)鎖為區(qū)間和站內(nèi)每個(gè)區(qū)段設(shè)置運(yùn)行方向，隨進(jìn)路的建立而建立，隨進(jìn)路的解鎖而清除。

2 UML2.0序列圖

UML2.0序列圖增加了12種組合片段[22]，包括loop，opt，alt，break，par，neg，ref等，增強(qiáng)了系統(tǒng)對(duì)象交互的需求分析與設(shè)計(jì)中的建模能力。

2.1 序列圖的形式化定義

定義1(序列圖)序列圖(SD, sequence diagram)通過一個(gè)十三元組表示SD=(O,E,S,R,M,P,C,OP,Fem,Feo,Fep,→,<)，其中，O是序列圖中對(duì)象的集合；E是序列圖中事件的集合；S是發(fā)送事件的集合；R是接收事件的集合,E=S∪R,S∩R=?；M是消息的集合，每條消息m(m∈M)與該條消息的發(fā)送事件!m(!m∈S)和接收事件?m(?m∈R)相關(guān)聯(lián)；P是組合片段的集合；C是組合片段執(zhí)行條件的集合；OP是操作域的集合，由組合片段各執(zhí)行條件表示；Fem表示E到M的函數(shù)關(guān)系，F(xiàn)em(e)∈M；Feo表示E到O的函數(shù)關(guān)系，F(xiàn)eo(e)∈O；Fep表示E到P的函數(shù)關(guān)系，F(xiàn)ep(e)∈P；→表示序列圖中消息的先后順序關(guān)系；?表示發(fā)送事件與接收事件的二元關(guān)系。

2.2 序列圖中對(duì)象的形式化定義

定義2(序列圖對(duì)象)序列圖中的對(duì)象通過一個(gè)六元組表示，O=(E,P,C,OP,N,Fep),其中，N表示事件發(fā)生的次序。

圖4 道岔單操命令的序列圖

圖4所示為道岔定操命令的序列圖及形式化定義，O聯(lián)鎖=({?m1,!m2,?m3,!m4}, {opt}, {null,道岔在反位}, {opt,道岔在反位}, {1,2,3,4},{(?m1,null),(!m2,opt[道岔在反位]),(?m3,opt[道岔在反位]),(!m4,null)})，其六元組關(guān)系見表2。

表2 聯(lián)鎖對(duì)象的六元組關(guān)系

3 序列圖形式化模型ETDFA生成方法

3.1 事件確定有限自動(dòng)機(jī)ETDFA

本文使用ETDFA的狀態(tài)遷移描述序列圖中的消息交互，實(shí)現(xiàn)序列圖中事件向?qū)ο蟮挠成洹顟B(tài)的一次遷移是指對(duì)象發(fā)送或接收消息后，從一個(gè)狀態(tài)轉(zhuǎn)移到另一個(gè)狀態(tài)，由事件發(fā)生的條件和事件本身構(gòu)成。序列圖中對(duì)象的交互過程可通過多個(gè)對(duì)象的積自動(dòng)機(jī)描述。

定義3(ETDFA)事件確定有限自動(dòng)機(jī)由一個(gè)七元組表示，M=(S,CM,EM,TCE,δ,s0,F)，其中，S表示狀態(tài)的集合，?s∈S；CM表示組合片段執(zhí)行條件的集合；EM表示事件集合；TCE表示狀態(tài)發(fā)生遷移的輸入，TCE={(c,e)|c∈CM,e∈EM}；δ表示狀態(tài)遷移函數(shù)，S×TCE→S；s0表示狀態(tài)機(jī)M的初始狀態(tài)，s0∈S；F表示狀態(tài)機(jī)M的終止?fàn)顟B(tài)集合，F(xiàn)?S。

3.2 序列圖的ETDFA模型生成算法

序列圖中每個(gè)對(duì)象的信息交互對(duì)應(yīng)一個(gè)事件確定有限自動(dòng)機(jī)ETDFA，其流程如圖5所示。

圖5 SD對(duì)象生成ETDFA模型流程圖

3.2.1 創(chuàng)建s1子流程

創(chuàng)建狀態(tài)s1的流程如圖6所示。

圖6 創(chuàng)建狀態(tài)s1流程圖

3.2.2 處理后續(xù)事件子流程

當(dāng)對(duì)象的六元組定義中的num>1時(shí)，狀態(tài)si(i∈2,…,num)的創(chuàng)建具體過程分以下幾種情況：

(1)若存在以下任一種情況時(shí)，δ(si,si+1)=ei+1；

①ei、ei+1均不在組合片段內(nèi)；

②ei、ei+1在組合片段的相同操作域內(nèi)；

③ei為par組合片段內(nèi)當(dāng)前操作域的最后一個(gè)事件，ei+1為該組合片段內(nèi)下一有效操作域內(nèi)的第1個(gè)事件；

④ei為alt或par片段內(nèi)最后一個(gè)有效操作域的最后一個(gè)事件，ei+1為片段外的第1個(gè)事件；

⑤ei+1在par片段內(nèi)，ei在片段外。

(2)若存在以下任一種情況時(shí)，δ(si,si+1)=c/ei+1；

①ei+1在alt或opt或loop或break單組合片段內(nèi)，ei在該組合片段外；

②ei+1在多層alt的組合片段內(nèi)，ei在該組合片段外。

(3)若存在以下任一種情況時(shí),si+1為終止?fàn)顟B(tài)；

①若ei+1不在組合片段內(nèi)，且ei+2不存在；

②若ei+1為組合片段內(nèi)的最后一個(gè)事件，且ei+2不存在；

③若ei+2在alt組合片段內(nèi)，ei+1在組合片段外，且alt組合片段操作域的并集不是全集；

④若ei+2在組合片段內(nèi)，ei+1在組合片段外，且組合片段后無事件發(fā)生；

⑤若ei+1為break組合片段內(nèi)的最后一個(gè)事件，且break片段外未嵌套其他片段。

3.2.3 處理組合片段子流程

與組合片段相關(guān)的事件生成的狀態(tài)遷移主要分7種情況，見表3，各種情況的示例圖見圖7、圖8。

表3 組合片段相關(guān)的狀態(tài)遷移

圖7 組合片段示例1

圖8 組合片段示例2

若序列圖中存在neg組合片段，在生成對(duì)象的自動(dòng)機(jī)時(shí)，忽略該片段。

4 CBTC聯(lián)鎖軟件的ETDFA模型

4.1 辦理進(jìn)路順序圖

本文以辦理進(jìn)路為例，驗(yàn)證基于ETDFA的聯(lián)鎖軟件的形式化模型生成方法的實(shí)際可行性。

CBTC系統(tǒng)在CBTC模式下辦理進(jìn)路的UML順序圖及形式化定義見圖9。

圖9 CBTC模式辦理進(jìn)路UML順序圖

O聯(lián)鎖= ({!m2, ?m3,!m4, ?m5, !m6,?m7,! m8,!m9,!m10, !m11},{alt,opt,loop,alt,alt},{null,c1,c2,c3,c4,c5,c6,c7},{(alt,c1),(opt,c1&&c2),(loop,c1&&c2&&c3),(alt,c1&&c4),(alt,c1&&c4&&c5),(alt,c1&&c4&&c6),(alt,c1&&c7)},{1,2,3,4,5,6,7,8,9,10,11},{(?m1,null),(!m2,alt[c1]),(?m3,alt[c1]),(!m4,alt[c1]&&opt[c2]&&loop[c3]),(?m5,alt[c1]&&opt[c2]&&loop[c3]),(!m6,alt[c1]&&alt[c4]),(?m7,alt[c1]&&alt[c4]),(!m8,alt[c1]&&alt[c4]&&alt[c5]),(!m9,alt[c1]&&alt[c4]&&alt[c5]),(!m10,alt[c1]&&alt[c4]&&alt[c6]),(!m11,alt[c1]&&alt[c7])})，表4為聯(lián)鎖對(duì)象的六元組關(guān)系。

表4 聯(lián)鎖對(duì)象的六元組關(guān)系

4.2 聯(lián)鎖對(duì)象的ETDFA模型

使用第4節(jié)描述的ETDFA模型生成方法，CBTC聯(lián)鎖對(duì)象的ETDFA的創(chuàng)建過程為：

1)設(shè)置初始狀態(tài)s0；

2)輸入狀態(tài)遷移字母表：

TCE={(c,e)|c∈CM,e∈EM};

CM={(alt,c1),(opt,c1&&c2),(loop,c1&&c2&&c3),(alt,c1&&c4),(alt,c1&&c4&&c5),(alt,c1&&c4&&c6),(alt,c1&&c7)};

EM={!m2,?m3,!m4,?m5,!m6,?m7,!m8,!m9,!m10,!m11}

3)根據(jù)算法依次創(chuàng)建狀態(tài)s1，s2，…，s11，狀態(tài)s9、s10、s11屬于終止?fàn)顟B(tài)；

4)組合片段處理生成的狀態(tài)遷移。

生成的聯(lián)鎖對(duì)象的自動(dòng)機(jī)的七元組定義為：

M聯(lián)鎖=({s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11}, {CM},{EM},{CM×EM}, {δ(s0,?m1)=s1,

δ(s1,[c1]/!m2=s2),

δ(s2,[c1]/?m3)=s3,

δ(s3,[c1&&c2&&c3]/!m4)=s4,

δ(s4,[c1&&c2&&c3]/?m5)=s5},

δ(s5,[c1&&c4]/!m6)=s6,

δ(s3,[c1&&c4]/!m6)=s6,

δ(s6,[c1&&c4]/?m7)=s7,

δ(s7,[c1&&c4&&c5]/!m8)=s8,

δ(s8,[c1&&c4&&c5]/!m9)=s9,

δ(s5,[c1&&c4&&c6]/!m10=s10,

δ(s5,[c1&&c7]/!m11)=s11,

δ(s3,[c1&&c4&&c6]/!m10=s10,

δ(s3,[c1&&c7]/!m11)=s11},{s0},{s9,s10,s11})

圖10為聯(lián)鎖對(duì)象的ETDAF模型。

圖10 聯(lián)鎖對(duì)象ETDFA模型

5 結(jié)論

本文采用UML順序圖描述CBTC聯(lián)鎖系統(tǒng)的聯(lián)鎖邏輯，從順序圖中提取單個(gè)對(duì)象的相關(guān)信息，通過形式化模型生成方法獲得單個(gè)對(duì)象的ETDFA模型。本方法不僅為CBTC聯(lián)鎖軟件的設(shè)計(jì)與開發(fā)提供新思路，而且有助于安全苛求軟件的形式化驗(yàn)證與分析，提高聯(lián)鎖軟件的安全性和正確性。

[1]中華人民共和國鐵道部. TB/T 3027-2015 計(jì)算機(jī)連鎖技術(shù)條件[S].北京:中國鐵道出版社,2015.

[2]吳芳美.計(jì)算機(jī)聯(lián)鎖軟件基于測(cè)試的安全性評(píng)價(jià)基準(zhǔn)研究[J],鐵道學(xué)報(bào),2005,27(3):97-101.

[3]Nakamatsu K, Kiuchi Y, Chen W Y, et al. Intelligent railway interlocking safety verification based on annotated logic program and its simulator[A]. 2004 IEEE International Conference on Networking, Sensing and Control[C]. IEEE, 2004, 1: 694-699.

[4]Hon Y M, Kollmann M. Simulation and verification of UML-based railway interlocking designs[A].Automatic Verification of Critical Systems[C]. 2006: 168-172.

[5]CENELEC. EN50128-2011 Railway applications-Communication, signaling and processing systems-Software for railway control and protection systems[S].Brussels:CENELEC,2011.

[6]Ben Ammar B, Bhiri M T, Souquières J. Incremental development of UML specifications using operation refinements[J]. Innovations in Systems and Software Engineering, 2008, 4(3):259-266.

[7]李景峰,陳 平.基于Z規(guī)范的統(tǒng)一建模語言序列圖語義分析方法[J].西安電子科技大學(xué)學(xué)報(bào)(自然科學(xué)版),2003,30(4):519-524.

[8]Zhou X, Shao Z. ASM Semantic Modeling and Checking for Sequence Diagram[A]. ICNC[C]. 2009 (5): 527-530.

[9]Gan J, Zhang S, Wen B. Research of modeling method based on UML2. 0 and temporal logic[A]. 2009 1st International Conference on Information Science and Engineering (ICISE) [C]. IEEE, 2009: 5033-5036.

[10]Tribastone M, Gilmore S. Automatic translation of UML sequence diagrams into PEPA models[A]. QEST'08. Fifth International Conference on Quantitative Evaluation of Systems, 2008 [C]. IEEE, 2008: 205-214.

[11]Lima V, Talhi C, Mouheb D, et al. Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages[J]. Electronic Notes in Theoretical Computer Science, 2009, 254: 143-160.

[12]Li G, Yao S. Research on mapping algorithm of UML sequence diagrams to object Petri nets[A]. GCIS'09. WRI Global Congress on Intelligent Systems, 2009[C]. IEEE, 2009, 4: 285-289.

[13]Nematzadeh H, Deris S B, Maleki H, et al. Evaluating reliability of system sequence diagram using fuzzy Petri net[J]. Int’l Journal of Recent Trends in Enginnering,2009,1(1):142-147.

[14]Esparza J. Decidability and complexity of Petri net problems—an introduction[Z].Lectures on Petri Nets I: Basic Models. Springer Berlin Heidelberg, 1998: 374-428.

[15]Knapp A, Wuttke J. Model checking of UML 2.0 interactions[A].International Conference on Model Driven Engineering Languages and Systems[C]. Springer Berlin Heidelberg, 2006: 42-51.

[16]Harel D, Kleinbort A, Maoz S. S2A: A compiler for multi-modal UML sequence diagrams[A].International Conference on Fundamental Approaches to Software Engineering[C]. Springer Berlin Heidelberg, 2007: 121-124.

[17]Harel D, Maoz S. Assert and negate revisited: Modal semantics for UML sequence diagrams[J]. Software & Systems Modeling, 2008, 7(2): 237-252.

[18]Broy M, Jonsson B, Katoen J P, et al. Model-Based testing of reactive systems[M]. Berlin: Heidelberg Springer- Verlag, 2005:615-616.

[19]Lynch N A, Tuttle M R. An introduction to input/output automata[J]. CWI Quarterly,1988,2(3):219-246.

[20]趙曉峰.計(jì)算機(jī)聯(lián)鎖在CBTC系統(tǒng)中的兩種集成方式[J].鐵道通信信號(hào),2012,48(11): 26-29.

[21]凌祝軍.CBTC系統(tǒng)中的聯(lián)鎖技術(shù)研究[J].鐵道通信信號(hào),2009,45(9):12-14.

[22]Jim Arlow, Ila Neustadt.UML 2.0 和統(tǒng)一過程[M]. 方貴賓,胡輝良,譯.第二版.北京:機(jī)械工業(yè)出版社,2006.

Method for Generating CBTC Interlocking Software′s Formal System Model Using ETDFA

Gao Xuejuan1,Chen Qixiang2, Zheng Hongchang1

(1.Signal & Communication Business Unit, Zhuzhou CRRC Times Electric Co., Ltd., Zhuzhou 412001, China;2.College of Electronics and Electrical Engineering, Baoji Wenli University, Baoji 721000, China)

The safety and integrity level of Computer interlocking software in CBTC(communication based train control) system is SIL4, which is high security and high reliability software. The current widely used software testing and simulation results rely heavily on the selected test vector, to ensure high coverage of the test is very difficult. EN50128 strongly recommended SIL4 level of software using formal methods to complete the software requirements specification and software design, therefore, using formal methods to design software is an important way to build high reliability and high security software. This paper summarizes the existing integrated approaches and advantages and disadvantages of the interlocking subsystem in the CBTC system, and uses the ETDFA (event deterministic finite automata) model to realize the formal definition of upgrade type interlocking software, which ensures the correctness of the interlocking logic, and reduces the uncertainty description of the software. This paper takes creating route as an example to generate the ETDFA model of the interlocking object, and verifies the validity and feasibility of the method. This method not only provides new ideas for the design and development of CBTC interlocking software, but also contributes to the formal verification and analysis of security demanding software, and improves the security and correctness of interlocking software.

CBTC; interlocking software; ETDFA; formal method

2017-03-27；

2017-05-27。

高雪娟(1990-)，女，甘肅白銀人，碩士研究生，主要從事城軌信號(hào)系統(tǒng)方向的研究。

1671-4598(2017)12-0120-05

10.16526/j.cnki.11-4762/tp.2017.12.032

TP273

A