CBTC系统中无线局域网主要故障包括信道失效(Transmission errors)、链路中断(Connection losses)和越区切换(Handover), 含义见文献[19].

图1给出无线局域网双网冗余结构信道失效、链路中断、重连失败和越区切换的模型, 一个无线小区中正常工作的基站数量用库所 Pok中的标记表示, 初始值为 2, 表示两套网络的基站工作均能正常工作.本文的双网冗余机制中只要有一套基站工作正常即可, 即库所 Pok标记的数值为 1或 2, 网络均可正常工作. 1)库所 Pdegrade代表信道失效所处的状态, 变迁 Tdeg和 Tdegr分别代表信道发生失效和恢复正常的动作; 2)库所 Poffline代表链路发生中断的时候所处的状态, 变迁 Tdw和 Tdwr分别代表链路中断和恢复动作; 3)库所 Phf表示列车越区切换所处的状态, 变迁 Thf和 Thfr分别代表列车越区切换准备执行和执行的动作.图1中菱形为随机 Petri网中的普通变迁, 表示该动作的执行时间服从指数分布; 矩形为固定变迁, 表示该动作的执行时间服从Er-lang分布; 椭圆形为立即变迁, 表示该动作瞬间执行^[20].

图1

Fig.1

	Figure Option ViewDownloadNew Window
	图1 无线局域网双网结构模型Fig.1 Model of redundancy structure in wireless network

1)当发生信道失效时, 库所 Pok的标记转移至信道失效状态, 当信道失效恢复后, 库所 Pdegrade的标记转回至库所 Pok, 至此完成信道的状态从正常到失效再恢复到正常的过程; 2)当无线局域网发生链路中断故障时, 触发链路中断动作, 使 Pok的标记转移至库所 Pdown, 再经由中断检测变迁转移至链路中断状态, 若重新建立链接能够成功, 则库所 Poffline的标记应转移至库所 Pok; 3)当重新建立链接失败, 触发变迁 Tfail, 标记转回至 Poffline中, 至此完成链路从中断到重新建立链接的过程.4)当越区切换时, 触发变迁 Thf准备执行切换任务, 库所 Pok的标记转移至执行切换状态, 完成执行切换后, 标记返回至库所 Pok.

M (Pok)> 0表示无线局域网正常, 其中M即Mark, 表示某种状态标识, 网络失效的情况包括:M (Pdegrade)=2,M (Poffline)=2,M (Phf)=2,M (Pdegrade)=1∧ M (Poffline)=1,M (Pdegrade)=1∧ M (Phf)=1,M (Poffline)=1∧ M (Phf)=1.

令 a∈A={0, 1, 2}为一个无线小区内正常工作的基站数量 (a=0⇔M (Pok)=0, a=1⇔ M (Pok)=1; a=2⇔ M (Pok)=2).类似方法定义 b∈B={0, 1, 2}, b=0⇔M (Pdegrade)=0, b=1⇔ M (Pdegrade)=1, b=2⇔ M (Pdegrade)=2; c∈C={0, 1, 2}, c=0⇔ M (Poffline)=0, c=1⇔ M (Poffline)=1, c=2⇔ M (Poffline)=2; d∈D={0, 1, 2}, d=0⇔ M(P_hf)=0, d=1⇔ M (Phf)=1, d=2⇔ M (Phf)=2.通过四元组 {(a, b, c, d), a∈A, b∈B, c∈C, d∈D}定义了无线局域网所处的状态, 即信道失效、链路中断和越区切换^[19] .图2给出无线局域网双网冗余结构的可靠性模型.@根据上述分析可知状态(2, 0, 0, 0), (1, 1, 0, 0), (1, 0, 1, 0), (1, 0, 0, 1)为系统的正常状态, 其他状态为失效状态.本文中定义状态(2, 0, 0, 0)为 Z0, (1, 0, 1, 0)为 Z1, (1, 0, 1, 0)为 Z2, (1, 0, 0, 1)为 Z3.聚合状态(0, 2, 0, 0), (0, 1, 1, 0), (0, 1, 0, 1)为 Z4, (0, 1, 0, 1), (0, 0, 1, 1), (0, 0, 0, 2)为 Z5, (0, 1, 1, 0), (0, 0, 2, 0), (0, 0, 1, 1)为 Z6.状态 Z0表示系统正常工作, 状态 Z1, Z2, Z3表示一个小区内一个基站失效, 定义吸收状态 TC={Z4, Z5, Z6}, 瞬时状态 T={Z0, Z1, Z2, Z3}, 当可靠性模型进入吸收状态, 表示无线局域网第1次发生失效^{[21, 22]} .用 λdeg、λdw、λhf分别表示信道失效、链路中断和越区切换的速率; λdegr、λdwr、λhfr分别表示信道恢复正常、链路恢复链接、越区切换结束的速率, 根据图2所示.

图2

Fig.2

	Figure Option ViewDownloadNew Window
	图2 无线局域网双网结构的可靠性模型Fig.2 Reliability model of redundancy structure in wireless network

将无限小生成元矩阵Q和状态转移矩阵Z(t)用吸收状态T_C和瞬时状态T表示成分块矩阵的形式^[22]为

Q=OORVTC TTCT(1)Z(t)=IOS(t)T(t)TC TTCT(2)

式中:Q是无限小生成元矩阵, 所以矩阵外用T_C和T表示了按照T_C和T分块的部分; I为单位矩阵; O为全0矩阵; Z(t)=e^Qt.

设 R1=λdeg+λdw+λhf,则有

R=0000R10000R10000R1O(3)

设V₁=-2λ _deg-2λ _dw-2d_hf, 则有

V=V12λdeg2λhf2λdwμdeg(-R1-μdw)00μhf0(-R1-μdw)0μdw00(-R1-μdw)(4)

吸收状态 S(t)可以写成

St=V-1T(t)-IR(5)

由于系统初始状态为 Z0, 则吸收状态 S(t)第1行元素的和为系统到达吸收状态的概率, 那么无线局域网双网冗余结构的可靠性 R(t)为

Rt=1-S(t)(1)e(6)

式中:S(t)⁽¹⁾为矩阵S(t)第1行向量; e=[1 1 1]^T.

参考ETCS规范和相关文献[1, 23], 表1为本文建立的无线局域网故障模型中变迁速率的取值.

表1

Tab.1

表1(Tab.1)

表1 图2对应变迁速率取值 Tab.1 Value of transition rate in Fig.2 变迁 发生速率 说明 λdeg 0.007 33 信道失效速率 λdegr 3 失效恢复速率 λdw 2.77× 10-8 链路中断速率 λdwr 0.6 重新建链成功速率 λhf 0.004 越区切换发生速率 λhfr 3.3 系统硬件执行切换速率

表1 图2对应变迁速率取值 Tab.1 Value of transition rate in Fig.2

对于无线局域网单网结构本文给出类似的模型与算法, 由于篇幅有限这里不再叙述, 根据以上参数, 图3给出无线局域网双网和单网结构的可靠性对比.从图3中可以看出, 单网结构的可靠性随时间增加迅速下降, 而双网结构的可靠性在单网结构的可靠性下降至0时依然接近于0.5, 这是因为单网结构可靠的条件比双网结构苛刻.对于双网结构, 一套网络业务中断时, 备份的另一套网络提供业务, 整个网络就不会中断, 提升了可靠性.

图3

Fig.3

	Figure Option ViewDownloadNew Window
	图3 无线局域网双网结构与单网结构可靠性对比Fig.3 Comparison of reliability of redundancy structure and single structure in wireless network

无线局域网是一个开放透明的网络, 信息在其中传输时可能存在错误或隐患, 具体描述见文献[24].针对这些错误或隐患, 可以通过改变设备和系统配置等方式消除或减轻, 也可以使用如增加序列号、时间戳、超时、安全编码和加密技术等方式来避免, 同时还可以在应用时采取操作及运营措施来防御, 如人员培训和管理监督等.

本文参考EN 50159-2^[24]的建议, 不修改底层设备, 在无线局域网双网冗余结构之上的应用层增加一层安全通信协议, 构成列控-安全信息传输系统(China-Radio), 下面将建立China-Radio系统的模型并对其功能进行验证.

ASK-CTL是一种常见的时序逻辑表达式, 以时间先后顺序来描述事件, 在模型检验中得到了广泛应用^[14].本文将针对China-Radio系统建立的有色Petri网模型生成状态空间可达图, 将需要验证的安全性功能用ASK-CTL语言公式表达, 进而通过状态空间搜索可达图上是否存在满足待验证的安全性功能的状态, 结果为真则证明系统性质满足, 否则给出反例, 验证人员根据反例路径查找系统不能满足性质的原因, 进一步修改系统模型直到检验结果为真.本文依据的模型检验流程如图7所示.

图7

Fig.7

	Figure Option ViewDownloadNew Window
	图7 对China-Radio的模型检验流程Fig.7 Procedure of model checking for China-Radio

用模型检验方法验证系统的安全性时, 定义安全性为不期望的状态永远不会发生^[14].China-Radio运行在安全苛求系统中, 期望状态可以看成是安全状态, 那么安全性的验证算法如图8所示.

图8

Fig.8

	Figure Option ViewDownloadNew Window
	图8 安全性验证算法Fig.8 Safety verification algorithm

由于安全性指期望状态经过任何路径“ 肯定” 会出现, 即所有路径都会到达期望状态.而由于COTS的“ 黑盒” 特性, 无线局域网的信息传输信道并不一定是理想的, 可能存在异常情况如图6所示.从安全苛求的角度考虑, 以下验证信道存在异常时China-Radio的安全性, 如图9所示.

图9

Fig.9

	Figure Option ViewDownloadNew Window
	图9 China-Radio的安全性验证Fig.9 Safety verification of China-Radio

从验证结果可以看出, 不是所有路径都可以到达安全状态, 即期望状态“ 安全链接建立上” , 这是因为信道异常发生时, 不管China-Radio的状态转换到什么阶段都会停止运行.为了用模型检验证明这一结论, 可以搜索到China-Radio停止运行时所处状态的路径, 算法如图10所示.

图10

Fig.10

	Figure Option ViewDownloadNew Window
	图10 非安全状态原因查找算法Fig.10 Algorithm of searching for non-safe state

根据图10的查找算法, 图11首先查找出China-Radio停止运行时所处状态即非安全状态在模型可达图中的编号.

图11

Fig.11

	Figure Option ViewDownloadNew Window
	图11 非安全状态编号查找Fig.11 Searching for number of non-safe state

图12表示查找到达某一非安全状态的路径.

图12

Fig.12

	Figure Option ViewDownloadNew Window
	图12 到达非安全状态的路径Fig.12 Path to non-safe state

从图12最后一行可知, 图7表示的信道异常情况是导致出现非安全状态的原因, 这是因为信道异常时, 数据在传输过程中会丢失, 导致China-Radio不能完成安全链接.根据这一结果可重新修改下行信道的参数, 使异常状态不发生, 并再次进行模型检验, China-Radio的安全性验证结果如图13所示.验证结果看出修改信道参数后, China-Radio模型所有路径都能达到安全状态, 说明China-Radio是安全的.

图13

Fig.13

	Figure Option ViewDownloadNew Window
	图13 修改信道参数后China-Radio的安全性验证Fig.13 Safety verification for China-Radio after parameters modification

为了验证China-Radio的安全性, 本文简化了无线局域网的信道模型, 将信道看成一个透明传输通道, 对信道失效的处理机制是将传输的数据直接丢失, 验证结果表明增加安全通信协议的双网冗余无线局域网可以满足列控系统的需求.