应用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