Formal Method for Behavior Verification and Data Validation of Station Interlocking System
-
摘要: 车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性. 为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML (unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验证过程,结合给定场景联锁数据的有效性确认,发现并纠正系统需求及分析过程中造成的潜在行为缺陷;通过功能仿真与验收测试,进一步确认了通用模型与联锁数据的正确性. 结果表明:本文方法提高了基于模型开发过程的准确性与层次性,验证了系统通用行为状态,且结合公理验证,实现了联锁数据的确认,并能基于模型进行功能场景仿真与测试,从而可进一步提高系统通用功能原型的可靠性.Abstract: Station interlocking system is a typical safety-critical system driven by data, which needs to verify the system behavior and confirm the correctness of data in the development. After analyzing the design specifications of the interlocking system, the initial system model was built automatically by the UML (unified modeling language) diagram, with the system properties and event flows described by Event-B language on RODIN platform. Subsequently, the refinement policy was used for hierarchical modeling, and the proof obligations of each layer were proved by theorem and the properties of the system attributions were verified. Thus, a reliable universal function model was obtained. Using a real station yard, the axioms of the model were proved and the interlocking data were validated as well. According to the formal verification and data validation in a given scenario, the subtle defects generated in the analysis of the system requirements could be found and corrected. Finally, the functional simulation and acceptance testing confirmed the correctness of the general model and the interlock data. This method not only improves the accuracy and hierarchy of the model-based development, but also verifies the universal behavior state of the system. Combined with axiomatic verification, the validation of interlocking data is realized. The function scenario can be simulated and tested based on the model, which can further improve the reliability of the universal function prototype of the system.
-
Key words:
- station interlocking system /
- formal verification /
- theorem proving /
- data validation /
- functional simulation /
- testing
-
《中国制造2025》战略的落地实施给制造业转型升级指明了方向. 作为一种重要的基础加工行业,金属切削制造业正逐步向智能化、柔性化的精益制造方向发展. 无人化的“熄灯工厂”新模式正在加速推广应用. 高端数控机床作为制造业的核心加工设备,切削加工质量指标(如:表面粗糙度)是影响加工生产效率的主要因素. 加工质量状态监测系统能够保证产品一致性,其推广运用不仅能够提升工厂效益,也能降低废品率,提升资源有效转换比,为国家“双碳”战略目标作出贡献.
近年来,随着工业大数据时代的转型升级以及深度学习技术的发展[1],采用数据驱动的有监督深度学习、边缘计算[2]以及机器视觉图像处理方法等专业技术相结合的工业监测手段得到广泛应用. 刀具[3]、丝杠[4-5]等部件作为数控切削加工的关键零件,其退化过程直接影响加工质量和生产安全. 而在线监测作为重要的监测手段,能够适配金属切削加工现场的复杂监测环境.
对于加工制造业,传统的离线监测与定期维修方式极大地影响了工厂的生产效率. 目前,在许多传统机械加工过程中,工件加工质量的判定是使用触针式表面粗糙度计或者白光干涉仪等设备进行测量. 这些监测方式虽然准确,但离线测量方式并不适用于工厂车间的大批量测试,且测试采样区窄小,需要多次测试. 间接测量方法则在批量测试上具有一定优势,其通过传感器或者机器视觉方法获取监测信号,通过特征提取与分析对切削加工过程和工件质量进行评估,具有在机安装方便、测试效率高等特点.
目前有少量国外研究者对采用传统传感器监测信号的粗糙度间接监测方法进行了研究. Papandrea等[6]研究了基于声发射信号的硬车削加工过程的粗糙度识别与监测方法. Plaza等[7]研究了基于振动监测信号和奇异谱分析方法的粗糙度监测方法. Tangjitsitcharoen等[8]基于切削力信号特征,研究了球头刀铣削加工过程的粗糙度监测方法. 然而,考虑到实际加工过程振动、切削力、声发射等时序信号对安装位置的敏感性以及昂贵的信号采集与处理设备的局限性,直接观测加工表面纹理的监测方法是另一种可探索的监测手段. Rifai等[9]对卷积神经网络在铣削、车削粗糙度识别任务的可行性进行了研究. 然而,其研究缺乏针对在机监测模型的实时性和数据分布特性的优化.
本文基于此,提出了一种改进型轻量级卷积网络,采用代价敏感损失提升在不平衡数据上训练的鲁棒性. 基于铣削纹理图像的监测算法能够实现工件粗糙度的快速识别. 此外,提出模型对低质量现场数据的类间不平衡特性和环境噪声干扰具有较强鲁棒性.
1. 轻量级卷积模型
研究新一代基于深度学习、边缘计算的在线监测技术对数控加工中心等高端制造设备的生产效率提升和加工质量控制具有重要意义. 其相比传统机器学习方法的手工特征选择与设计,过程得到简化.
自2012年AlexNet[10]首个深度卷积网络在大规模图像数据集取得突破性进展后,残差网络[11]等研究避免了卷积网络结构训练过程易出现的梯度弥散现象,使得训练大型神经网络模型成为现实. 而轻量级卷积结构(如:基于可分离卷积的MobileNet[12],结构见图1)的发展为基于边缘计算的工业监测提供了基础. ImageNet数据集[10]为模型预训练提供了支持.
2. 立铣粗糙度在线监测模型
铣削粗糙度在线监测模型示意如图2. 算法具体包括图像预处理、图像校正、纹理识别. 图中:FFT-LPF算子为傅里叶频域变换后低通滤波处理算子,Ra为粗糙度值.
首先,对采集原始图像预处理. 具体包括2个步骤,即采用直方图均衡化方法增强图像、基于纹理图像的清晰度评价判断并采集大于设定阈值的样本,清晰度评价指标包括拉普拉斯(Laplace)算子、FFT-LPF算子2种,阈值(thresh)根据不同工况适当调整.
然后,图像校正模块实现了一种基于匹配点信息对比的位姿校正方法. 基于方向HOG特征的工件区域(目标区域)检测算子对工件区域进行检测;并基于单应性矩阵位姿估计方法,对相机安装偏差进行校正,实现对校正后工件纹理图样的采集与数据集制作.
最后,设计了一种轻量级卷积网络结构,采用代价敏感的交叉熵损失函数模型能够稳定、鲁棒地实现对不同粗糙度刀具加工表面的图样进行纹理特征提取与识别. 下面将进一步阐述各模块的功能实现.
2.1 图像预处理
图像预处理是保证原始图像数据质量的必要手段,而合理的曝光、对焦参数能够实现高质量成像.
2.1.1 直方图均衡化
灰度直方图描述了灰度分布情况. 对于尺寸为M(长) × N(宽)的工件纹理灰度图像,其灰度直方图为
p(rm)=nm/(M×N),rm∈[0,255], (1) 式中:$ p\left( {{r_{\rm{m}}}} \right)$为灰度级$ {r_{\rm{m}}}$在图像中的概率分布,$ {n_{\rm{m}}}$为灰度值统计.
扩展灰度分布动态范围能够改善局部亮度分布. 对于图像的直方图均衡化过程,可以描述为一个线性变换过程T(rm),如式(2).
T(rm)=(255−1)K∑rm=0p(rm), (2) 式中:K为目标灰阶值.
图3(a)、(b)为纹理图像经过标准化后,采用直方图均衡化处理前后差异比较.
2.1.2 清晰度评价
无参考图像质量评价采用清晰度指标来对采集图像优劣进行评判. 常用的清晰度评价指标包括:Laplace函数、熵值函数和FFT-LPF均值函数.
图像空间频域信息描述了纹理图像在长、宽方向上的变化剧烈程度. 类似于Laplace变换的高通低阻特性,通过FFT-LPF,能够表征纹理图像中纹理色块变化程度(轮廓、角点). 其中,二维离散傅里叶变换得到的空间频域成分为
F(k,l)=M−1∑m=0N−1∑n=0f(m,n)e−2πn(kmM+lnN), (3) 式中: $ m、{{n}}$为离散时域变量,k、l为离散频域变量,$ f(m,n)$为图像空间域矩阵像素值.
对于任意$ F\left( {k,l} \right)$,可通过将空间频域与相应的基函数相乘并将结果相加得到. 通过高通低阻滤波后,将图像信息从空间频域恢复到空间域,变换过程表示为
f(m,n)=1N2M−1∑k=0N−1∑l=0F(k,l)e2πn(kmM+lnN). (4) 2.2 图像校正
采集得到的纹理图像,需要进一步通过校正方法,减小其安装误差带来的特征扰动的影响. 为实现在线数据采集,设计了一种快速图像校正方案. 首先,基于改进的低感度参数设置的HOG算子,检测并识别工件目标区域,并通过单应性矩阵方法对相机安装误差进行校正.
2.2.1 基于HOG算子的目标区域检测
如图4所示,根据不同划分区间$ \left( {{\theta _1},{\theta _2}} \right)、\left( {{\theta _3},{\theta _4}} \right)、 \left( {{\theta _5},{\theta _6}} \right)、\cdots \cdots$得到梯度方向信息,将局部图像信息的梯度统计编码为特征向量F. 通过基于特征的智能算法(支持向量机)方法,即可实现对目标区域的提取.
其中,色块梯度的方向描述了图像某一方向灰度阶变化快慢. 当图像局部色块存在边缘等纹理信息时,体现为较大某一方向上的梯度值较大. 对于图像长(M)、宽(N)方向上的梯度$ G_{m} $和$ G_{{n}} $分别为
[GmGn]=[∂f(m,n)∂m∂f(m,n)∂n]. (5) 则梯度幅值为$ \sqrt {G_m^2 + G_n^2} $,梯度方向$ \theta = \arctan ({G_n}/{G_m})$.
对于灰度阶纹理图像矩阵,宽度方向梯度:$ \partial f({\text{•}})/\partial m = f\left( {m + 1,n} \right) - f\left( {m,n} \right)$,长度方向梯度:$ \partial f({\text{•}})/ \partial n = f\left( {m,n + 1} \right) - f\left( {m,n} \right)$.
获得色块梯度信息后,通过直方图信息统计、特征向量构建,输入智能模型后即可实现对关键区域的识别.
2.2.2 考虑安装误差的在线图像校正
通过尺度不变特征变换(SIFT)算子识别不同批次采集图像的特征点,与标准安装距离下的测试进行比较,求解单应性矩阵,实现图像安装误差的校正.
根据尺度不变特征变换(SIFT)算子获取的标准图像与在线监测纹理图像之间的匹配点对$ \left( {{x}_{i}},x_{i}^{*} \right) {{x}_{i}}\in {{\mathbb{P}}^{1}},x_{i}^{*}\in {{\mathbb{P}}^{2}},i=1,2,\cdots$,即可计算标准图像到在线监测图像之间的投影变换. 单应性矩阵即根据2D匹配点之间变换关系的估计,使得对于$ {{x}_{i}}\in {{\mathbb{P}}^{1}},x_{i}^{*}\in {{\mathbb{P}}^{2}}$投影空间内的点对匹配误差最小.
尺度归一化后的单应性矩阵通过点检测与匹配得到的多个已知点对,即可求解出单应性矩阵估计值. 图5为图像间的点对算法匹配的结果.
由于实际匹配过程难免出现误匹配,使得投影变换$ f_{\rm{t}} $估计不准确. 采用随机采样一致性(RANSAC)方法,能够有效滤除一定误匹配点对,从而计算得到相对较优的单应性矩阵估计值.
2.3 基于代价敏感损失与可分离卷积的识别模型
铣削纹理提供了丰富的切削质量监测信息. 按照纹理特征提取特点,常用的工件加工表面纹理特征可分为一阶统计算子(如灰度阶直方图)、多阶统计学算子(如灰度共生矩阵算子[13]、Voronoi多边形[14])以及空间频域特征[15-16]. 这些纹理识别算子为粗糙度识别提供了大量可用特征[17-18]. 但这些特征却难以全面和完备表征多工况情形下的工件表面纹理特性.
深度学习方法借助其较强的高维非线性表征能力,能够较好解决这一问题. 基于代价敏感损失的深度卷积网络,进一步解决了存在类间不平衡现象的低质量数据的模型训练问题. 并且在准确性上,模型通过充分训练,与经典深度卷积模型在高质量数据训练情形下效果相当.
此外,通过在普通卷积网络模型中替换部分标准卷积为深度可分离卷积,可以提升模型的推理速度. 深度可分离卷积包括两个部分:逐点卷积和逐通道卷积. 在逐通道卷积中,单个卷积核只实现输入特征图(FM)的一个通道的卷积运算. 在完成逐通道卷积后,叠加得到中间特征层后再对其做点卷积运算,得到输出FM. 其具体计算步骤如下:
步骤1 逐通道卷积:采用一个尺寸为$ {k_c} \times {k_c} \times 1$的卷积核,对一个尺寸为$ {H_i} \times {W_i} \times {c_1}$的输入FM的每个通道进行卷积操作,得到尺寸为$ {H_m} \times {W_m} \times {c_1}$的中间特征图;
步骤2 逐点卷积:采用$ {c_2}$个尺寸为$ 1 \times 1 \times {c_1}$尺寸的卷积核对中间特征图作点卷积操作,得到尺寸为$ {H_o} \times {W_o} \times {c_2}$的输出FM.
对于单个深度可分离卷积,其通过逐通道卷积和点卷积两个分解操作得到了采用$ c_{2} $个尺寸为$ {k_c} \times {k_c} \times {c_1}$的卷积核做普通卷积的相同输出FM,而其乘法运算次数得到大幅度降低. 假设两种卷积方法的卷积核共移动了$ {N_k} \times {N_k}$次,以乘法运算量作为量化指标,则两种计算方法效率比值可表示为
RDS−C=c1k2cNk2+c2c1N2kc2k2cc1Nk2=1c2+1k2c. (6) 图6可视化了多代价敏感损失不同调制因子($ \gamma $)下损失值与预测结果置信度之间的关系. 普通交叉熵损失函数难以训练样本数量少的类别中难区分的样本. 而代价敏感损失通过调整不同类权值,控制模型对各类的训练损失,能够较好解决这一问题.
3. 提出算法验证与分析
3.1 铣削纹理采集与监测实验
本实验所用的加工纹理数据包括粗糙度对比样块以及切削加工实验的工件数据. 实验所获得的工件不同倍率、粗糙度的加工纹理数据如图7所示. 铣削实验采集了整体式立铣刀(C1)和方肩立铣刀(C2)不同工况下的纹理图像,并采用触针式粗糙度仪进行了测量与图像标注,如图8所示.
在刀具磨损退化监测实验中,采集了3种工况设置下,刀具进展性磨损下的工件表面粗糙度情况. 工况参数设置如表1所示,C1刀具的测量值如图9所示. 据工件生产加工的工艺的范围要求,将数据划分为符合要求的A类和不符合要求的B类. 划分方式为指标Ra在3次测量中两次小于或等于2的划分为A类,大于则为B类.
表 1 监测实验工况设置明细Table 1. Details of monitoring experiment工况 主轴转速/
(r·min−1)进给速度/
(mm·min−1)切削深度/mm 刀具
类型机床
型号1 3000 200 1 C1 KVC650 2 4000 200 1 C2 KVC650 3 2000 200 0.5 C2 VMC850 3.2 纹理在线采集与校正
图10为几种不同清晰度评价阈值设置方式得到的纹理数据采集比较. 在采集过程中光源持续照明时间为2 s. 镜头和相机以恒定速度完成对焦过程.
相比于Laplace函数计算方法,熵值和FFT-LPF均值方法调焦过程指标变化波动较少,有利于对焦过程的快速调整. 但熵值方法敏感性过低,难以收敛到最佳点. 因而,选用FFT-LPF均值方法折中敏感性与单调性的优势,适合在线监测.
3.3 纹理识别实验分析
深度可分离的代价敏感深度卷积网络在训练过程的可视化如图11所示. 可以看到,在训练初期,模型训练集损失值下降过程存在轻微波动,收敛效果相比基于标准卷积的神经网络稍差. 但可以观察到,由于DP (dropout)层以及全局最大池化层的正则化项作用,损失逐渐趋于稳定.
表2所示为深度可分离卷积结构的消融实验结果, 表中,$ {\alpha} $为可分离卷积结构在模型中替代标准卷积结构的比率. 可以观察到,采用深度可分离卷积结构能够在模型精度损失较小情况下有效提升模型的推理速度.
表 2 可分离卷积结构的消融实验结果Table 2. Ablation experiment for separable convolution模型结构 推理速度/ms 准确率/% 普通卷积 33.7 77.6 可分离卷积(α=0.2) 25.2 75.7 可分离卷积 2(α=0.3) 25.1 72.1 如表3所示为采用普通交叉熵损失和代价敏感损失函数的模型在不同参数设置下的精准率(P)和召回率(R)的比较结果. 其中:工况1下的刀具失效模式为剧烈磨损,磨损各个阶段持续时间相对较为均匀(数据类间比率为1∶1.2);由于工况2与工况1的数据分布情况类似,不做附加比较;工况3下刀具失效模式为崩刃,各个阶段持续时间上具有差异,类间不均衡比率较大(数据类间比率为1∶3.1). 可以观察到代价敏感损失有效提升了模型存在显著类间不均衡情况(工况3)下的识别准确性.
表 3 普通交叉熵损失和代价敏感损失函数测试结果Table 3. Test results of standard cross-entropy and cost-sensitive loss% 损失函数 精准率 召回率 工况 1 工况 3 工况 1 工况 3 普通交叉熵 79.1 77.5 80.2 78.3 代价敏感损失 78.7 79.9 80.6 80.3 图12所示的基于对比实验的混淆矩阵测试与可视化结果说明了深度卷积模型采用代价敏感损失函数的必要性. 模型A采用代价敏感损失函数,模型B采用普通交叉熵损失函数. 可以观察到,采用代价敏感损失的模型具有更小的类间差异.
为验证提出方法相比手工特征的优势,表4给出了最终模型与GLCM (gray level co-occurence matrix) + SVM (支持向量机类算法)方法的比较结果. GLCM + SVM和GLCM + RF (随机森林算法)方法采用4种典型的灰度共生矩阵纹理特征[19]分别作为支持向量机和随机森林模型的数据输入. 支持向量机方法测试了Linear核函数和RBF核函数. 并给出了P、R和识别速度的比较,计算如式(7)、(8).
表 4 模型性能评估测试Table 4. Model performance evaluation方法 P/% R/% 计算时间/(s·帧−1) GLCM + SVM (RBF) 73.7 65.3 0.208 GLCM + SVM (linear) 73.2 65.5 0.208 GLCM + RF 73.4 65.1 0.208 提出方法 81.6 86.2 0.150 P=Ntp/(Ntp+Nfp)×100%, (7) R=Ntp/(Ntp+Nfn)×100%, (8) 式中:Ntp为真阳性数量,Nfp为假阳性数量,Nfn为假阴性数量.
可以观察到:RF和SVM在计算时间上基本不具备差异性,这是由于算法主要耗时在纹理图像的灰度共生矩阵特征计算上. 其中,采用不同核函数的高斯核(RBF)、线性核(linear)以及RF决策部分的350张图像计算耗时分别为7.50、7.98、1.99 ms,相对于特征计算过程其耗时几乎可以忽略. 而提出模型在考虑模型加载时间的情况下,仍然能够达到0.150 s/帧的实时计算性能.
4. 结 论
本文针对加工表面粗糙度在机监测问题提出了基于代价敏感损失函数与轻量级卷积的深度学习模型的铣削加工粗糙度识别方法. 对于铣削纹理采集的自动校正、对焦算子进行了探究. 考虑已加工表面纹理信息的轻量级卷积网络能够适配在机监测的实时计算需求;而代价敏感损失函数能够有效提升轻量级模型在数据分布波动情形下的鲁棒性,缩短调试周期.
SIFT算子在铣削纹理图像匹配上具有较好的性能. 并通过消融实验,验证了提出模型所采用的代价敏感损失函数与可分离卷积网络结构方法用于在机监测的优越性. 算法在工件纹理图像数据上进行粗糙度识别实验,结果验证了提出方法的准确性和高效性,相比传统的手工特征智能方法,准确率和运算速度提升明显. 在收敛性上,相比于普通卷积神经网络,模型收敛较快,但过早收敛也容易陷入局部最佳点,或者出现过拟合现象等,该方面仍有待进一步研究.
-
表 1 模型各层精化内容
Table 1. Refinement of the model
精化层级 引入对象 第 1 层 建立列车对象,构造进路相关事件基本功能流程,如建立进路、进路正常解锁、进路取消、进路人工延时解锁和进路故障解锁等 第 2 层 建立进路类型、进路方向、轨道区段类型、列车类型和敌对进路的定义,描述与进路、轨道区段、列车相关的功能与安全属性 第 3 层 建立道岔对象,将道岔锁闭和解锁流程同步在建立进路和解锁进路事件中 第 4 层 添加道岔的位置信息,增加道岔转动的计时约束,完善与道岔相关的事件 第 5 层 建立信号机对象,完善人工延时解锁、取消进路等事件 第 6 层 定义进路进程,增加信号设备故障和修复等事件,完善故障解锁流程 表 2 模型证明义务的证明情况统计
Table 2. Proving statistics of model proof obligations
条 文件名称 总数 自动 手动 已修正 未通过 C0 1 1 0 0 0 C1 6 5 1 0 0 C2 4 2 2 0 0 C3 2 2 0 0 0 C4 6 6 0 0 0 C5 5 3 2 0 0 C6 0 0 0 0 0 M0 0 0 0 0 0 M1 80 49 31 0 0 M2 59 17 42 0 0 M3 46 17 29 0 0 M4 118 41 77 0 0 M5 146 61 85 0 0 M6 237 218 19 0 0 总计 710 422 288 0 0 表 3 举例车站联锁表
Table 3. Interlocking table of the example station
方向 进路 信号机 道岔 轨道区段 出站轨道区段 敌对信号 敌对进路 迎面敌对 进路编号 名称 显示 发车进路 股道 Ⅰ至 X SⅠ L 1、3 1/3DG Q_1 X 1 — 7 股道 Ⅱ至 X SⅡ L 1、(3) 1/3DG Q_1 X 2 — 8 股道 Ⅲ至 X SⅢ L (1)、{3} 1/3DG Q_1 X 3 — 9 股道 Ⅰ至 S XⅠ L 2、4 2/4DG Q_2 S 4 — 10 股道 Ⅱ至 S XⅡ L (2)、{4} 2/4DG Q_2 S 5 — 11 股道 Ⅲ至 S XⅢ L 2、(4) 2/4DG Q_2 S 6 — 12 注:信号机中,L表示绿灯;道岔中,1表示1# 道岔在定位,(1)表示1# 道岔在反位,{1}表示1# 道岔带动在定位,其余类推;轨道区段中,1/3DG表示1~3轨道区段,2/4DG表示2~4轨道区段. 表 4 公理验证结果
Table 4. Verification of axioms
条 文件名称 总数 自动 手动 已修正 未通过 C0 7 3 4 0 0 C1 22 7 14 0 1 C1_1 6 3 3 0 0 C2 15 2 13 0 0 C3 9 3 6 0 0 C4 20 16 4 0 0 C5 14 0 14 0 0 C6 0 0 0 0 0 总计 93 34 58 0 1 -
王恪铭,王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报,2019,54(3): 573-578,603.WANG Keming, WANG Zheng. Modeling and verification of control system specification for railway level crossings based on formal method[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 573-578,603. International Electrotechnical Commision. Functional safety of electrical/electronic/programmable electronic safety-reared systems: IEC 61508[S]. Geneva: European Committee for Electrotechnical Standardization. 2005. KHAN U, AHMAD J, SAEED T, et al. On the real time modeling of interlocking system of passenger lines of Rawalpindi Cantt train station[J]. Complex Adaptive Systems Modeling, 2016, 4(1): 1-33. doi: 10.1186/s40294-016-0028-5 VU L H, HAXTHAUSEN A E, PELESKA J. Formal modelling and verification of interlocking systems featuring sequential release[J]. Science of Computer Programming, 2017, 133: 91-115. doi: 10.1016/j.scico.2016.05.010 BONACCHI A, FANTECHI A, BACHERINI S, et al. Validation process for railway interlocking systems[J]. Science of Computer Programming., 2016, 128: 2-21. doi: 10.1016/j.scico.2016.04.004 HANSEN D, SCHNEIDER D, LEUSCHEL M. Using B and ProB for data validation projects[C]//Inernational Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. [S.l.]: Springer, 2016: 167-182. ABRIAL J R. Train system[M]//Modeling in Event-B. Cambridge: Cambridge University Press, 2013: 508-549. 国家铁路局. 铁路车站计算机联锁技术条件: TB/T 3027—2015[S]. 北京: 中国铁道出版社. 2015. 张传东. EVENT-B方法在铁路车站联锁规范形式化建模与验证中的应用研究[D]. 成都: 西南交通大学, 2017. ZHANG Chuandong, WANG Keming, WANG Xia, et al. Interlocking data[DB/OL]. [2019-08-16]. https://github.com/abidefei/Model_Verification_Data_Validation_Interlocking_EventB. SNOOK C, HOANG T S, DGHYAM D, et al. Behaviour-driven formal model development[M]//Formal Methods and Software Engineering. Cham: Springer International Publishing, 2018: 21-36. 期刊类型引用(5)
1. 苏昕宇,梁志国,张宏扬,王海峰. 基于深度学习的联锁测试序列推荐方法. 铁道标准设计. 2024(09): 192-199 . 百度学术
2. 王霞,王恪铭,徐扬,唐伟健. 基于形式化方法的平交道口控制系统安全设计. 西南交通大学学报. 2023(01): 109-116 . 本站查看
3. 袁飞军,王圣根,王亚飞. 基于信号集中监测系统的联锁试验. 铁道通信信号. 2023(02): 82-85 . 百度学术
4. 刘宁,韩程,王峥,侯锡立,王恪铭. 基于B方法的道岔控制系统形式化建模与验证. 铁路通信信号工程技术. 2022(06): 5-11 . 百度学术
5. 王若冲,韩笑,严紫薇. 基于UML模型的道岔控制安全逻辑分析及设计实现. 智慧轨道交通. 2022(05): 77-80 . 百度学术
其他类型引用(8)
-