應用ETDFA生成CBTC聯鎖軟件形式化模型的方法

高雪娟, 陳啟香, 鄭鴻昌

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

應用ETDFA生成CBTC聯鎖軟件形式化模型的方法

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

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

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

CBTC；聯鎖軟件；ETDFA；形式化方法

0 引言

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

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

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

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

1 CBTC聯鎖軟件

1.1 聯鎖集成方式

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

表1 不同集成方式的CBTC聯鎖系統對比

圖1為以兼容型方式集成聯鎖的結構框圖，圖2為以升級型方式集成聯鎖的結構框圖。

本文基于升級型集成方式的聯鎖實現CBTC聯鎖系統的ETDFA模型。

圖1 兼容型集成聯鎖框圖

圖2 升級型集成聯鎖框圖

1.2 CBTC聯鎖系統功能

圖3為升級型集成方式的聯鎖系統結構圖。

圖3 升級型集成方式聯鎖系統結構圖

CBTC聯鎖系統與傳統聯鎖的不同主要有以下幾個方面：

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

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

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

4)信號顯示：CBTC聯鎖系統在CBTC模式下，若信號機使用傳統點燈方式，當信號機發生故障，對運營效率產生極大影響，而且，在CBTC模式下，信號開放不檢查進路內區段的空閑狀態，違背了計算機聯鎖技術條件中的規定，因此，在CBTC模式下，信號顯示采用滅燈方式，簡化了系統的運用條件。

5)保護進路：類似大鐵的延續進路，為避免列車因停車誤差而造成安全隱患，CBTC系統為接車進路設置“保護進路”，一般為進路終端停車點信號機內方一個區段。當接車進路建立、列車駛入觸發區段時，“保護進路”自動建立。“保護進路”的解鎖方式與大鐵延續進路類似。

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

2 UML2.0序列圖

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

2.1 序列圖的形式化定義

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

2.2 序列圖中對象的形式化定義

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

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

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

表2 聯鎖對象的六元組關系

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

3.1 事件確定有限自動機ETDFA

本文使用ETDFA的狀態遷移描述序列圖中的消息交互，實現序列圖中事件向對象的映射。狀態的一次遷移是指對象發送或接收消息后，從一個狀態轉移到另一個狀態，由事件發生的條件和事件本身構成。序列圖中對象的交互過程可通過多個對象的積自動機描述。

定義3(ETDFA)事件確定有限自動機由一個七元組表示，M=(S,CM,EM,TCE,δ,s0,F)，其中，S表示狀態的集合，?s∈S；CM表示組合片段執行條件的集合；EM表示事件集合；TCE表示狀態發生遷移的輸入，TCE={(c,e)|c∈CM,e∈EM}；δ表示狀態遷移函數，S×TCE→S；s0表示狀態機M的初始狀態，s0∈S；F表示狀態機M的終止狀態集合，F?S。

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

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

圖5 SD對象生成ETDFA模型流程圖

3.2.1 創建s1子流程

創建狀態s1的流程如圖6所示。

圖6 創建狀態s1流程圖

3.2.2 處理后續事件子流程

當對象的六元組定義中的num>1時，狀態si(i∈2,…,num)的創建具體過程分以下幾種情況：

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

①ei、ei+1均不在組合片段內；

②ei、ei+1在組合片段的相同操作域內；

③ei為par組合片段內當前操作域的最后一個事件，ei+1為該組合片段內下一有效操作域內的第1個事件；

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

⑤ei+1在par片段內，ei在片段外。

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

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

②ei+1在多層alt的組合片段內，ei在該組合片段外。

(3)若存在以下任一種情況時,si+1為終止狀態；

①若ei+1不在組合片段內，且ei+2不存在；

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

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

④若ei+2在組合片段內，ei+1在組合片段外，且組合片段后無事件發生；

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

3.2.3 處理組合片段子流程

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

表3 組合片段相關的狀態遷移

圖7 組合片段示例1

圖8 組合片段示例2

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

4 CBTC聯鎖軟件的ETDFA模型

4.1 辦理進路順序圖

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

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

圖9 CBTC模式辦理進路UML順序圖

O聯鎖= ({!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為聯鎖對象的六元組關系。

表4 聯鎖對象的六元組關系

4.2 聯鎖對象的ETDFA模型

使用第4節描述的ETDFA模型生成方法，CBTC聯鎖對象的ETDFA的創建過程為：

1)設置初始狀態s0；

2)輸入狀態遷移字母表：

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)根據算法依次創建狀態s1，s2，…，s11，狀態s9、s10、s11屬于終止狀態；

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

生成的聯鎖對象的自動機的七元組定義為：

M聯鎖=({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為聯鎖對象的ETDAF模型。

圖10 聯鎖對象ETDFA模型

5 結論

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

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

[2]吳芳美.計算機聯鎖軟件基于測試的安全性評價基準研究[J],鐵道學報,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規范的統一建模語言序列圖語義分析方法[J].西安電子科技大學學報(自然科學版),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]趙曉峰.計算機聯鎖在CBTC系統中的兩種集成方式[J].鐵道通信信號,2012,48(11): 26-29.

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

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

1671-4598(2017)12-0120-05

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

TP273

A