Processing math: 100%
  • ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

基于形式化方法的道口控制系统规范建模与验证

王恪铭 王峥

张先玉, 陈勇, 张余, 杨华. 无人机通信中的资源分配及部署位置联合优化[J]. 西南交通大学学报, 2024, 59(4): 917-924. doi: 10.3969/j.issn.0258-2724.20230400
引用本文: 王恪铭, 王峥. 基于形式化方法的道口控制系统规范建模与验证[J]. 西南交通大学学报, 2019, 54(3): 573-578, 603. doi: 10.3969/j.issn.0258-2724.20180607
ZHANG Xianyu, CHEN Yong, ZHANG Yu, YANG Hua. Joint Optimization of Resource Allocation and Deployment Location in Unmanned Aerial Vehicle-Assisted Communication[J]. Journal of Southwest Jiaotong University, 2024, 59(4): 917-924. doi: 10.3969/j.issn.0258-2724.20230400
Citation: 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. doi: 10.3969/j.issn.0258-2724.20180607

基于形式化方法的道口控制系统规范建模与验证

doi: 10.3969/j.issn.0258-2724.20180607
基金项目: 国家自然科学基金资助项目(71502146,61673320);中央高校基本科研业务费资助项目(2682017ZT12)
详细信息
    作者简介:

    王恪铭(1981—),男,讲师,博士,研究方向为形式化建模与验证、运输系统优化,E-mail:kmwang@swjtu.edu.cn

  • 中图分类号: TP301.2;U213.8;U298.5

Modeling and Verification of Control System Specification for Railway Level Crossings Based on Formal Method

  • 摘要: 为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证. 基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用UML图方法并结合精化策略建立了系统各层的Event-B语言模型. 通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型. 最后,通过不变式冲突与死锁检验进一步确认了模型的正确性. 研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.

     

  • 近几十年来,借助于信息技术的快速迭代和制造工艺的飞速发展,无人机在军事、运输、农业等领域广泛应用[1-3]. 无人机具有价格低廉、部署方便、移动灵活、控制简单等优势,将其融入移动通信系统已成为提升通信服务质量的重要举措,得到了学界和工业部门的广泛关注[4-6]. 无人机既可作为移动用户,利用现有的地面基础通信网络对其提供指令、传输数据等业务,提高无人机通信的可靠性和有效性;同时,无人机也可充当空中基站或中继节点,为特定地区或时段提供不间断、宽覆盖的通信服务,并利用良好的空域传输条件满足高速率、低延迟的通信需求. 无人机通信作为现有通信系统的重要补充,克服了地面基础设施的诸多限制,在提高网络覆盖率、改善网络服务质量、增进系统可靠性等方面具有重要意义. 然而,无人机通信也面临诸多挑战. 一方面,受尺寸、载荷、功率等限制,无人机通信的频谱和发射功率有限,需要有效分配通信资源;另一方面,无人机的灵活性和移动性对节点部署提出了高要求,需要合理设计轨迹或位置,以提升网络性能[7-9].

    无人机通信系统的资源分配和轨迹/位置优化问题备受关注. 文献[10]研究了多无人机作为移动基站的通信系统中用户分配和无人机轨迹联合优化方法;文献[11]针对不同的用户需求,以提升用户公平性为目标,研究无人机通信系统中的带宽、功率和轨迹联合优化问题;文献[12]利用博弈论研究任务驱动下的无人机通信系统频谱分配;文献[13-14]探讨了无人机作为中继节点的网络资源分配和轨迹优化等问题. 正交频分多址接入(orthogonal frequency division multiple access, OFDMA)作为高效的多载波通信技术,已成为多个商用系统的标准多用户接入方式[15-16]. 文献[17]以无人机作为空中基站工作在OFDMA模式下,研究无人机轨迹和网络资源联合优化方法,提升网络公平性; 文献[18]研究无人机辅助蜂窝通信系统中的资源分配和轨迹联合优化问题,提出迭代优化算法实现网络容量的最大化;文献[19]基于智能超表面(intelligent reflecting surface, IRS)辅助的OFDMA无人机通信系统,研究无人机轨迹、网络资源、IRS配置的联合优化问题. 上述文献均是基于理论容量进行优化分析,实际应用中,主流的无人机系统和无线通信系统均为数字通信方式,数据速率和可靠性是系统设计的重要依据. 文献[20]将一定数据速率和误码率作为OFDMA无人机网络的限制条件,以最小化传输功率为目标,研究子载波分配、调制模式选择和轨迹联合优化问题,但尚未考虑功率分配等因素,也未进一步考虑提升网络速率、公平性等指标.

    基于上述问题,本文以最大化用户最小传输速率为目标,在一定的误码率要求下,考虑网络资源分配和无人机位置联合优化问题. 所建问题为混合整数优化问题,直接求解难度较大. 为解决变量间的耦合性,将联合优化问题分解为2个子优化问题,并通过适当变换转化为0-1线性优化和凸优化问题,利用迭代优化方法进行求解. 最后,通过实验仿真和算法对比验证所提算法的有效性和公平性.

    考虑将无人机作为空中基站的场景,系统模型如图1所示. 在通信服务区域内,存在一个空中悬停无人机作为空中基站,同时为M个地面用户提供通信服务. 为描述方便,设定用户索引集合为M={1,2,,m,,M}. 特别地,为提升频谱效率,设定无人机基站工作在OFDMA工作模式,系统总带宽为B,均分为N个子载波,单个子载波带宽Δf=B/N,子信道索引集合为N={1,2,,n,N}. 基站会根据用户的需求及信道质量分配一定数量的子信道,且同一子信道仅能分配到至多1个用户. 因此,不同用户之间不存在信道间干扰. 定义子信道分配变量αmn,若子信道n分配给用户mαmn=1,反之,αmn=0. 另外,为提升系统性能,基站可根据一定的算法自适应调整各子信道的功率分配和调制方式. 不失一般性,本文考虑正交幅度调制(quadrature amplitude modulation,QAM),选定的调制维度集为cn{1,2,4,6},即系统可自适应选择BPSK、QPSK、16QAM和64QAM 4种调制方式. 在实际应用中,可根据具体情况选定合适的维度集或其他调制方式.

    图  1  所考虑的无人机通信系统模型示意
    Figure  1.  System model of considered UAV-assisted communication

    设定无人机悬停高度为H,其平面坐标q=(xU,yU). 类似地,假定地面用户的垂直高度为0,相应地,用户m的平面坐标wm=(xm,ym).

    相比于地面通信系统,无人机通信具有良好的视距到达特性,无人机—地面信道极少会受到障碍物及非视距分量的影响,信道传播质量主要取决于直达链路. 类似于文献[21-22],本文选择直达链路为信道传播模型. 基于自由空间信道传播模型,UAV与用户m之间的信号功率衰减系数为[21-24]

    hm=β0H2+qwm2, (1)

    式中:β0为单位距离(1 m)处的信号功率衰减量.

    假定各子信道独立选择QAM调制方式,用户m的接收信号误码率为Pem,若αmn=1,根据文献[25],用户m利用子信道n实现可靠接收信息符号所需的信噪比为

    fm(cn)={12[Q1(Pem)]2,cn=1,13[Q1(Pem4)]2(2cn1),cn=2,4,6, (2)

    式中:Q1(x)为式(3)所示Q函数的逆函数.

    Q(x)=12πxet22dt. (3)

    进一步地,UAV利用信道n服务于用户m所需的功率下界可表示为

    plimmn=αmnfm(cn)δ20Δfhm, (4)

    式中:δ20为用户m处的噪声功率谱密度.

    网络公平性是衡量通信系统性能的重要指标,能够确保稳定可靠的通信服务. 本文将提升网络的公平性作为系统设计的主要指标. 为得到优化的系统设计方案,首先需要对问题进行建模:将最大化用户最小信息速率作为优化目标,以有限的发射功率、子信道、调制方式作为限制条件,实现对子信道分配、功率分配、调制方式选择及无人机位置的联合优化. 为表示方便,优化变量可表示为:A={αmn,mM,nN}C={cn,nN}P={pn,nN}q=(xU,yU)pn为第n个子信道功率. 相应地,联合优化问题可建模为

    P0max{A,C,P,q}minRm s.tNn=1αmncn=Rm,mM,Mm=1αmn1,nN,PemPemax,mM,Nn=1pnPT,αmn{0,1},mM,nN,cn{1,2,4,6},nN,

    式中:Rm为用户m获取的信息速率,Pemax为误码率上限,PT为UAV总发射功率限制.

    明显地,所建立的优化问题P0为一个混合整数非线性优化问题,并且αmncncnq之间互相耦合. 因此,很难直接求解该问题.

    为解决优化问题P0中的变量耦合问题,采用迭代优化的方法进行求解. 利用梯度下降法将优化问题分解为2个子问题:子信道分配及调制模式识别优化问题、功率分配和无人机位置优化问题. 然后,利用迭代优化求解,得到优化的系统设计方案.

    子信道分配系数αmn和调制模式选择系数cn之间互耦,直接联合优化两类参数难度很大. 由于cn取值为有限的4个离散值,因此,可将表达式αmnfm(cn)变换为式(5).

    qm(bmn)=ρm1bmn+3ρm2b2mn+15ρm2b3mn+63ρm2b4mn, (5)
    ρm1=12[Q1(Pem)]2, (6)
    ρm2=13[Q1(Pem4)]2, (7)
    04s=1bsmn1, (8)

    式中:ρm1ρm2为系数;bmn{0,1},为二进制变量,且应满足式(8)所示约束条件.

    通过上述变换,可将优化变量αmncnbsmn替代表示,因此,子信道分配及调制模式选择优化问题可表示为

    P1max {A,C}min Rm,s.t.Nn=1rmn=Rm,mM,rmn=bmn+2b2mn+4b3mn+6b4mn,mM,nN,04s=1bsmn1,mM,nN,0Mm=14s=1bsmn1,nN,pmnqm(bsmn)δ20Δfhm,mM,nN.

    优化问题P1为一个0-1整数线性规划问题,可通过成熟的算法(CPLEX或者MOSEK等)予以求解.

    从信息速率的形式上看,在满足功率、误码率等约束条件下,用户的信息速率由子信道选择系数和调制模式选择系数决定. 因此,子问题1决定了用户的信息速率,在分配方案不变、满足相应约束条件情况下,用户信息速率不会随着功率及位置发生变化. 另一方面,由信道传输模型可知,无人机和用户节点之间的距离直接影响了用户的信噪比,进而通过调整调制模式改变接收的信息速率. 因此,功率分配及无人机位置联合优化问题可将最小化最大传输距离作为优化目标,通过调整功率和无人机位置,尽量提升最低信道衰减值,同时又满足子问题1分配方案所需的功率及误码率约束. 基于上述考虑,功率分配及无人机位置联合优化子问题可建模为

    P2min {P,q}max Dm,
    s.t.H2+qwm2=Dm,mM,pnqm(bmn)δ20Δf(H2+qwm2)β0,mM,nN,Nn=1pnPT,αmn{0,1},mM,nN,cn{1,2,4,6},nN.

    进一步,引入松弛变量η=max Dm,将问题变换为

    P3min {P,q}η,
    s.t.H2+qwm2η,mM,pnqm(bmn)δ20Δf(H2+qwm2)β0,mM,nN,Nn=1pnPT,αmn{0,1},mM,nN,cn{1,2,4,6},nN.

    明显可见,问题P3为凸优化问题,因此,可通过标准算法(CVX软件包等)进行求解.

    总体而言,直接求解通信资源分配及位置联合优化问题难度较大,可通过梯度下降法将其转变为2个子优化问题,即3.1节和3.2节所述的问题,进而可通过迭代优化的方式进行求解[26],直至算法收敛. 相关算法流程为:

    1) 输入:无人机通信网络设定的误码率要求Pem,无人机最大传输功率限制PT,调制模式选择类型cn;最大迭代次数Numi和收敛门限ε;无人机初始位置q0=(xU,yU)和初始功率分配方案P0={pn,nN},子信道分配方案A0={αmn,mM,nN},调制模式选择方案C0={cn,nN}.

    2) 基于参数A0C0P0q0计算得到用户速率初值Rm,0及可获取的最小用户速率ϕ0=minRm,0.

    3) for i=1:Numi

    4) 基于第i−1次迭代功率分配方案Pi1、无人机位置qi1,建立子信道分配及调制模式选择优化模型,利用二进制线性规划优化算法求解得到第i次迭代的子信道分配方案Ai和调制模式选择方案Cb.

    5) 基于AiCi,建立功率分配及无人机位置联合优化模型,利用凸优化算法求解得到优化变量Piqi.

    6) 基于参数AiCiPiqi计算得到第i次迭代的用户速率Rm,i及可获取的最小用户速率ϕi=minRm,i.

    7) 计算判断:若i=Numi或者(ϕiϕi1)/ϕi1ε迭代停止退出;否则,i=i+1,迭代继续.

    8) End For

    9) 输出:优化的资源分配及无人机位置方案(AiCiPiqi).

    为验证所提算法的有效性,本节通过设计不同条件下的仿真,利用结果比对验证所提算法的性能. 不失一般性,设定实验仿真条件为:服务区域为半径500 m的圆形区域,无人机以一定的高度悬停在空中,作为空中基站为服务区域内的K个用户提供通信服务,且用户均匀分布在服务区域内;另外,无人机的可用子载波个数、总带宽及最大发射功率均受限. 关键参数设置如表1所示. 仿真时,选定具有代表性的均匀分配算法作为对比对象:无人机的水平位置设置在所有服务用户的中心点,即xU=xm/M,yU=ym/M;子信道平均分配至M个用户,即每个用户占用的子信道数目为N/NMM;各子信道功率一致,均为pn=PT/PTNN;各子信道均选定能够满足误码率要求的最高阶调制方式. 所提算法的迭代参数可设定为Numi=20次,ε=0.01.

    表  1  部分关键系统仿真参数
    Table  1.  Some key system simulation parameters
    参数 数值
    M/个 20
    H/m 100
    N/个 100
    B/MHz 10
    β0/dB −50
    δ20/(dBm·Hz−1) −169
    Pemax 104
    PT/dBm 22
    下载: 导出CSV 
    | 显示表格

    网络各节点的平面部署情况示意如图2所示,从图中可见,20个地面用户均匀分布在服务区域内,假设无人机初始位置均选择部署在网络中心区域内. 在UAV部署位置优化中,本文设定的优化目标是:尽量减小最大传输距离,降低信号的最大衰减量. 图2中用户9更靠近服务区域的边界,UAV会朝着更靠近用户9的方向部署,同时受到其他用户的限制,UAV的部署不会偏离中心位置太远. 因此,所提算法能够考虑到网络公平性,能够平衡各用户的通信服务需求.

    图  2  网络节点部署位置示意
    Figure  2.  Deployment location of network nodes

    相应地,图3为所提算法得到的子载波分配方案. 图中,蓝色矩形表示“未分配”,黄色矩形代表“分配”,余图同. 明显可见,相比均匀分配算法,本文所提算法对子信道的分配方案实际调整较少,仅用户2和用户12增加了1个子信道,各分配6个子信道;用户14减少了2个子信道,仅分配3个子信道,其余用户仍为5个子信道. 这是由于在本系统设定中子信道数量相对于用户数量较少,可调整的自由度不足,为满足用户的公平性,需要子信道数目保持一定的稳定性. 用户14与UAV空中基站的距离最近,具有最优的信道质量,因此,利用较少数量的子信道既可达到较高的信息传输速率.

    图  3  无人机各子信道的优化分配情况
    Figure  3.  Optimal sub-channel allocation of UAV

    图4表示均匀分配算法及本文所提优化算法所采用的调制方式选择方案. 从图中可以发现:2种算法均没有选择BPSK调制,仅有用户14选择64QAM调制. 因此,所选仿真系统设定中,大量的用户适用于QPSK、16QAM调制方式. 基站可通过调整各子信道功率,使得较多的子信道适用于高阶调制方式. 2种算法的功率分配方案如图5所示. 由于本文设定功率为连续可调变量,功率域的自由度较大,系统可通过合理分配各信道功率使得较多的子信道适用于更高阶的数字调制方式,进而提升用户速率. 为提升所提算法的适用性,也可通过适当的调整,将功率设定为固定可调档位选择,得到离散的功率调整方案. 另外,从图5可以发现,对于同一用户的不同子信道,系统分配的功率不同. 这是因为本文所提算法中功率分配仅是一类变量,当算法获得优化结果后即停止迭代. 事实上,若将同一用户的子信道功率一致增加为约束条件,即可获得均匀的功率分配方案.

    图  4  调制方式选择
    Figure  4.  Modulation mode selection

    利用得到的通信资源分配及无人机位置优化方案,通过计算得到各用户信息速率. 2种算法下用户获取速率的对比如图6所示. 由于本文所提的优化算法综合考虑了频域、功率域和空间域,变量的自由度较大,能够综合利用各空间的参数改进系统的总体性能. 因此,本文所提算法能够有效提高用户的最小获取速率,改善网络的公平性.

    图  5  功率分配方案
    Figure  5.  Power allocation schemes
    图  6  用户获取速率
    Figure  6.  Achievable user rate

    图7为不同误码率要求及不同发射功率限制下的系统最小获取用户速率性能对比,横坐标表示误码率上限及最大功率限制,即(Pemax,PT),其中,PT的单位为dBW. 由图可见,系统最小获取信息速率会随着设定误码率的增大呈增长趋势,也会随着最大发射功率的增大呈增长趋势;所提优化算法能极大提升系统可获取的最小信息速率. 另一方面,最小获取用户速率呈阶梯状增加,这是由于在数字调制方式中,信息速率仅与调制方式及信噪比有关,而信噪比在一定范围内,所选的调制方式可保持一定的稳定性,因此,速率变化为离散变化,而非连续变化.

    图  7  不同误码率及发射功率下最小获取用户速率
    Figure  7.  Minimum achievable user rates with different BERs and transmitted powers

    无人机的高度也是系统设计中需要考虑的重要因素,实际情况中无人机高度会直接影响系统的覆盖范围和可获取的信息速率. 本文中仅考虑通信直达链路,信号仅与传播距离有关,因此,未考虑非直达链路造成的性能损失. 图8显示了系统获取的最小信息速率与无人机高度的关系曲线. 由图8可见,均匀分配算法下,利用设定的系统参数获取的最小速率未发生变化,这是因为均匀分配会使得最小速率用户获得足够的带宽和功率,确保信道在一定变换范围内保持稳定的信息获取速率. 相应地,本文优化算法中,系统最小获取速率会随着无人机高度的提升呈下降趋势,这与预期结果一致:随着无人机高度的增加,信号传输衰减会随之增大,从而造成信息速率的降低. 同时,最小获取信息速率阶梯状下降,这与图7中的变化趋势相似:信息速率在一定信噪比变换范围内保持稳定.

    图  8  不同无人机高度下的用户最小获取信息速率
    Figure  8.  Minimum achievable user rates under different UAV heights

    事实上,以上仿真实验仅是针对某种用户分布情况下做出的针对性分析对比. 下一步,可针对不同的用户节点分布展开分析比对,或者利用传输信道的瞬时或统计特性进行研究,使本文所提算法更具针对性和普适性.

    本文解决了基于OFDMA模式的无人机通信系统中的通信资源及无人机位置联合优化问题. 首先,以提升系统用户的公平性为目标,将联合优化问题建模为子信道、功率、误码率限制下的最大-最小问题;之后,利用迭代优化的方法将联合优化分解为2个子优化问题,通过适当的变换将子优化问题转变为标准的0-1整数线性规划和凸优化问题分别求解. 仿真结果证实所提算法能有效提升用户最小获取速率,改善系统的服务质量.

  • 图 1  铁路道口控制系统示意

    Figure 1.  Schematic diagram of control system for railway level crossings

    图 2  道口控制系统中的事件流程

    Figure 2.  Events flows of control system for railway level crossings

    图 3  初始模型中的场景文件

    Figure 3.  Context file in the initial model

    图 4  初始模型中的UML图

    Figure 4.  UML diagram in the initial model

    图 5  初始模型中的机器文件

    Figure 5.  Machine file in the initial model

    图 6  基于特性的不变式验证

    Figure 6.  Property-based invariants verification

    图 7  添加事件的防卫条件

    Figure 7.  Additional guards of event

    图 8  精化过程中的证明义务统计

    Figure 8.  Statistics of proof obligation in the refinement processes

    图 9  道口异常处理流程

    Figure 9.  Exception-handling process of the railway level crossings

    图 10  新增对应的异常处理流程不变式验证

    Figure 10.  Additional invariants verification of exception-handling process

    表  1  模型精化过程

    Table  1.   Refinement processes of the model

    精化层级引入对象
    第1层引入栏门、控制器对象,建立栏门开启与关闭的过程事件.
    第2层引入时间对象,建立系统时钟,完善栏门接收控制器命令后开启与关闭过程的时间要求.
    第3层引入列车、信号灯对象,增加列车接近、列车逼近、列车离去道口事件与信号灯转换事件,完善道口系统执行过程.
    第4层引入列车接近、逼近计时,完善控制器的时间约束.
    下载: 导出CSV
  • 国家安全生产监管管理总局. 铁路运输行业基本情况[R/OL]. (2014-06-17)[2018-01-04]. http://www.chinasafety.gov.cn/newpage/Contents/Channel_21500/2014/0617/236238/content_236238.htm
    European Union Agency for Railways. Railway safety performance in the european union[R/OL]. (2016-09-13)[2018-01-04]. http://www.era.europa.eu/Document-Register/Documents/Railway%20Safety%20Performance%202016%20final%20E.pdf
    Eurostat. Rail accident fatalities in the EU[R/OL]. (2017-02-10)[2018-01-04]. http://ec.europa.eu/eurostat/statistics-explained/index.php/Rail_accident_fatalities_in_the_EU#Further_Eurostat_information
    贾明涛,王海星,肖贵平. 铁路道口安全影响因素分析及对策[J]. 安全与环境学报,2006,6(6): 123-126. doi: 10.3969/j.issn.1009-6094.2006.06.033

    JIA Mingtao, WANG Haixing, XIAO Guiping. Safety analysis on highway-railway crossings[J]. Journal of Safety and Environment, 2006, 6(6): 123-126. doi: 10.3969/j.issn.1009-6094.2006.06.033
    GHAZEL M, EL-KOURSI E M. Two-half-barrier level crossings versus four-half-barrier level crossings:a comparative risk analysis study[J]. IEEE Transactions on Intelligent Transportation Systems, 2014, 15(3): 1123-1133. doi: 10.1109/TITS.2013.2294874
    MEKKI A, GHAZEL M, TOGUYENI A. Validation of a new functional design of automatic protection systems at level crossings with model-checking techniques[J]. IEEE Transactions on Intelligent Transportation Systems, 2012, 13(2): 714-723. doi: 10.1109/TITS.2011.2178238
    SALMANE H, KHOUDOUR L, RUICHEK Y. A video-analysis-based railway-road safety system for detecting Hazard situations at level crossings[J]. IEEE Transactions on Intelligent Transportation Systems, 2015, 16(2): 596-609.
    LARSEN P G, LARSEN P G, BICARREGUI J, et al. Formal methods:practice and experience[J]. ACM Computing Surveys, 2009, 41(4): 1-40.
    CENELEC. IEC61508: Functional safety of electrical/electronic/programmable electronic safety-reared systems[S/OL]. European Committee for Electrotechnical Standardization. [2018-01-04]. https://webstore.iec.ch/preview/info_iec61508-0%7Bed1.0%7Db.pdf
    SUN J, SUN S, LI K, et al. Efficient algorithm for traffic engineering in cloud-of-things and edge computing[J]. Computers & Electrical Engineering, 2018, 69(7): 610-627.
    LEFFINGWELL D, WIDRIG D. Managing software requirements: a use case approach[M]. New Jersey: Addison-Wesley, 2003: 10-40
    国家铁路局. 铁路站内道口信号设备技术条件: GB10493—2018[S]. 北京: 中国标准出版社, 2018: 3-5
    中国铁路总公司. 铁路道口管理办法: 铁总运[2013]121号[S/OL]. 北京: [s.n.], 2013: 10-19. [2018-01-04]. https://wenku.baidu.com/view/fe0322d649649b6648d74789.html
    ABRIAL J R. Modeling in Event-B: system and software engineering[M]. Cambridge: Cambridge University Press, 2010: 217-219
    BUTLER M. Reasoned modelling with Event-B[C]//Engineering Trustworthy Software Systems, SETSS 2016. Cham: Springer, 2016: 51-109
    WANG K. Rail level crossing DATA[CP/OL]. [2018-5-21]. https://github.com/abidefei/RailLevelCrossing_EventB
    ZHU C, BUTLER M, CIRSTEA C. Refinement of timing constraints for concurrent tasks with scheduling[C]//International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Cham: Springer, 2018: 219-233
  • 期刊类型引用(5)

    1. 李铮,郑泽熙,李亮,王萌,邓晶雪. 匈牙利铁路平交道口封锁方案设计与实现. 铁道通信信号. 2024(05): 92-97 . 百度学术
    2. 郑泽熙,李亮,邓晓鹏,邓晶雪,段鹏宇. 匈牙利铁路区间道口与公路路口联动方案研究. 铁道通信信号. 2024(06): 85-90 . 百度学术
    3. 赵大地,王恪铭. 基于状态图转形式化B模型的安全苛求系统开发方法. 计算机工程. 2024(11): 173-186 . 百度学术
    4. 王霞,王恪铭,徐扬,唐伟健. 基于形式化方法的平交道口控制系统安全设计. 西南交通大学学报. 2023(01): 109-116 . 本站查看
    5. 王恪铭,王霞,程鹏,刘宁,张传东. 车站联锁系统行为验证与数据确认的形式化方法. 西南交通大学学报. 2021(03): 587-593+613 . 本站查看

    其他类型引用(11)

  • 加载中
图(10) / 表(1)
计量
  • 文章访问数:  479
  • HTML全文浏览量:  228
  • PDF下载量:  14
  • 被引次数: 16
出版历程
  • 收稿日期:  2018-07-16
  • 修回日期:  2018-09-18
  • 网络出版日期:  2019-03-30
  • 刊出日期:  2019-06-01

目录

/

返回文章
返回