高雪娟, 陳啟香, 鄭鴻昌

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

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

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

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

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

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

0 引言

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

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

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

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

1 CBTC聯(lián)鎖軟件

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2 UML2.0序列圖

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

2.1 序列圖的形式化定義

定義1(序列圖)序列圖(SD, sequence diagram)通過一個十三元組表示SD=(O,E,S,R,M,P,C,OP,Fem,Feo,Fep,→,<)，其中，O是序列圖中對象的集合；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 序列圖中對象的形式化定義

定義2(序列圖對象)序列圖中的對象通過一個六元組表示，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)鎖對象的六元組關(guān)系

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

3.1 事件確定有限自動機ETDFA

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

定義3(ETDFA)事件確定有限自動機由一個七元組表示，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)機M的初始狀態(tài)，s0∈S；F表示狀態(tài)機M的終止?fàn)顟B(tài)集合，F(xiàn)?S。

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

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

圖5 SD對象生成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)對象的六元組定義中的num>1時，狀態(tài)si(i∈2,…,num)的創(chuàng)建具體過程分以下幾種情況：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.2.3 處理組合片段子流程

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

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

圖7 組合片段示例1

圖8 組合片段示例2

若序列圖中存在neg組合片段，在生成對象的自動機時，忽略該片段。

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

4.1 辦理進路順序圖

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

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

圖9 CBTC模式辦理進路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)鎖對象的六元組關(guān)系。

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

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

使用第4節(jié)描述的ETDFA模型生成方法，CBTC聯(lián)鎖對象的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)鎖對象的自動機的七元組定義為：

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)鎖對象的ETDAF模型。

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

5 結(jié)論

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

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

[2]吳芳美.計算機聯(lián)鎖軟件基于測試的安全性評價基準(zhǔn)研究[J],鐵道學(xué)報,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é)報(自然科學(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]趙曉峰.計算機聯(lián)鎖在CBTC系統(tǒng)中的兩種集成方式[J].鐵道通信信號,2012,48(11): 26-29.

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

[22]Jim Arlow, Ila Neustadt.UML 2.0 和統(tǒng)一過程[M]. 方貴賓,胡輝良,譯.第二版.北京:機械工業(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-)，女，甘肅白銀人，碩士研究生，主要從事城軌信號系統(tǒng)方向的研究。

1671-4598(2017)12-0120-05

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

TP273

A