Loading [MathJax]/jax/output/SVG/jax.js
  • 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]. 西南交通大学学报, 2022, 57(2): 392-400, 424. doi: 10.3969/j.issn.0258-2724.20200530
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: LI Yao, ZHANG Xiaoxia, GUO Jin, ZHANG Yadong. Modeling Method for Testing Railway Signal System Software[J]. Journal of Southwest Jiaotong University, 2022, 57(2): 392-400, 424. doi: 10.3969/j.issn.0258-2724.20200530

铁路信号系统软件测试建模方法

doi: 10.3969/j.issn.0258-2724.20200530
基金项目: 国家自然科学基金(61703349)
详细信息
    作者简介:

    李耀(1985—),男,博士研究生,研究方向为铁路信号系统安全关键软件测试,E-mail:ly_9967@163.com

    通讯作者:

    张晓霞(1961—),女,教授,研究方向为通信技术可靠性,E-mail:xxzhang@uestc.edu.cn

  • 中图分类号: U283

Modeling Method for Testing Railway Signal System Software

  • 摘要:

    针对铁路信号系统软件测试模型不能系统地描述测试需求的问题,提出风险时间状态机建模方法. 首先,分析铁路信号系统软件测试建模的特点,并提出建模需求;然后,以有限状态机理论为研究基础,在有限状态机的变迁和状态中分别扩展出时钟和风险等级元素,提出风险时间状态机建模方法,满足功能逻辑、时间约束和风险等级3个方面的建模需求,采用Z规格说明语言给出风险时间状态机的形式化定义和格局转移机制;最后,以计算机联锁系统中的道岔转换功能为例,建立风险时间状态机测试模型,并与时间自动机建模方法进行了对比,结果表明,建模方法上,所建立风险时间状态机比时间自动机节省62%的变迁数,描述能力更强,能够满足铁路信号系统软件测试的建模需求.

     

  • 近几十年来,借助于信息技术的快速迭代和制造工艺的飞速发展,无人机在军事、运输、农业等领域广泛应用[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.  Main testing process of railway signal system software

    图 2  有限状态机模型

    Figure 2.  Example of finite state machine

    图 3  道岔子系统RTSC模型

    Figure 3.  RTSC model of switch subsystem

    图 4  道岔子系统风险矩阵

    Figure 4.  Risk matrix of switch subsystem

    图 5  道岔子系统TA模型

    Figure 5.  TA model of switch subsystem

    图 6  RTSC模型与TA模型对比

    Figure 6.  Comparison between RTSC model and TA model

    表  1  道岔子系统信号含义

    Table  1.   Meaning of signals in switch subsystem

    信号含义信号含义信号含义
    e1 定位请求 e4 定位需求 e7 道岔定位
    e2 道岔转换 e5 道岔锁闭 e8 转换成功
    e3 转换超时 e6 反位请求 e9 选排一致
    下载: 导出CSV

    表  2  DRTSCDTA 对比

    Table  2.   Comparison between DRTSC and DTA

    模型构件/个状态/个变迁/条信号/个
    DRTSC1111911
    DTA4244918
    下载: 导出CSV

    表  3  RTSC与测试需求的关系

    Table  3.   Relationship between RTSC and test requirements

    特性功能性实时性风险
    状态迁移 × ×
    层次性 × ×
    并发性 × ×
    时间约束 × ×
    风险等级 × ×
    注:“√”表示RTSC特性满足建模需求;“×”则相反.
    下载: 导出CSV
  • [1] 上官伟,胡福威,袁敏,等. 基于弹复力效应的列控车载设备可靠性分析方法[J]. 铁道学报,2018,40(6): 75-82. doi: 10.3969/j.issn.1001-8360.2018.06.010

    SHANGGUAN Wei, HU Fuwei, YUAN Min, et al. Reliability analysis method for on-board equipment of train control system based on resilience effect[J]. Journal of the China Railway Society, 2018, 40(6): 75-82. doi: 10.3969/j.issn.1001-8360.2018.06.010
    [2] 梁茨,郑伟,李开成,等. 基于路径优化算法的测试序列自动生成及验证[J]. 铁道学报,2013,35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009

    LIANG Ci, ZHENG Wei, LI Kaicheng, et al. Automated generation of test cases and sequences based on path optimization algorithm[J]. Journal of the China Railway Society, 2013, 35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009
    [3] 赵晓宇,杨志杰,吕旌阳. 基于有色Petri网的车载设备模式转换测试序列生成方法[J]. 中国铁道科学,2017,38(4): 115-123. doi: 10.3969/j.issn.1001-4632.2017.04.16

    ZHAO Xiaoyu, YANG Zhijie, LU Jingyang. Test sequence generation method of mode transition for on-board equipment based on colored petri net[J]. China Railway Science, 2017, 38(4): 115-123. doi: 10.3969/j.issn.1001-4632.2017.04.16
    [4] 袁磊,吕继东,刘雨,等. 一种全覆盖的列控车载系统测试用例自动生成算法研究[J]. 铁道学报,2014,36(8): 55-62. doi: 10.3969/j.issn.1001-8360.2014.08.010

    YUAN Lei, LYU Jidong, LIU Yu, et al. Research on model-based test case generation method of onboard subsystem in CTCS-3[J]. Journal of the China Railway Society, 2014, 36(8): 55-62. doi: 10.3969/j.issn.1001-8360.2014.08.010
    [5] 魏柏全,吕继东,陈柯行,等. 基于TAIO变异的CTCS-3列控系统测试案例生成方法[J]. 西南交通大学学报,2020,55(5): 937-945, 962. doi: 10.3969/j.issn.0258-2724.20180078

    WEI Baiquan, LYU Jidong, CHEN Kexing, et al. Mutation timed automata with input and output-based method of generating test suites for Chinese train control system level 3[J]. Journal of Southwest Jiaotong University, 2020, 55(5): 937-945, 962. doi: 10.3969/j.issn.0258-2724.20180078
    [6] 曹雅鑫. 基于UML状态图的列控中心轨道电路编码功能测试用例生成方法研究[D]. 成都: 西南交通大学, 2017.
    [7] 黄平霞. 基于UML的地铁联锁软件测试用例生成方法的研究[D]. 兰州: 兰州交通大学, 2016.
    [8] 徐中伟. 安全软件测试理论与技术的研究及其在铁路信号安全软件测评中的实现[D]. 上海: 同济大学, 2000.
    [9] 王硕,郭进,张亚东. 面向列控系统安全软件黑盒测试的危险分析方法[J]. 铁道科学与工程学报,2019,16(3): 590-595.

    WANG Shuo, GUO Jin, ZHANG Yadong. Hazard analysis method for security software black-box testing of train control system[J]. Journal of Railway Science and Engineering, 2019, 16(3): 590-595.
    [10] 李耀,陈荣武,郭进,等. 基于TSSM的城市轨道交通CBTC区域控制器建模与验证[J]. 西南交通大学学报,2015,50(1): 27-35. doi: 10.3969/j.issn.0258-2724.2015.01.005

    LI Yao, CHEN Rongwu, GUO Jin, et al. Modeling and verification of TSSM-based CBTC zone controller for urban rail transit[J]. Journal of Southwest Jiaotong University, 2015, 50(1): 27-35. doi: 10.3969/j.issn.0258-2724.2015.01.005
    [11] 李耀,郭进,杨扬,等. 铁路信号安全关键软件形式化建模[J]. 铁道学报,2017,39(9): 74-80. doi: 10.3969/j.issn.1001-8360.2017.09.011

    LI Yao, GUO Jin, YANG Yang, et al. Formal modeling of railway signal safety critical software[J]. Journal of the China Railway Society, 2017, 39(9): 74-80. doi: 10.3969/j.issn.1001-8360.2017.09.011
    [12] HSIUNG P A, LIN Y H. Modeling and verification of safety-critical systems using safecharts[C]//Formal Techniques for Networked and Distributed Systems - FORTE 2005. Berlin: Springer Berlin Heidelberg, 2005: 290-304.
    [13] AMMANN P, OFFUTT J. Introduction to Software Testing[M]. Cambridge: Cambridge University Press, 2017: 3-24.
    [14] 张曙光. CTCS-3级列控系统总体技术方案[M]. 北京: 中国铁道出版社, 2008.
    [15] 铁道部科学技术司, 铁道部运输局. CTCS-3级列控系统测试案例(V3.0): 科技运[2009] 59号[S]. 北京: [出版者不详], 2009.
    [16] 饶畅,李楠,张亚东,等. 铁路信号安全关键软件的组合测试序列集约简[J]. 西南交通大学学报,2020,55(3): 596-603. doi: 10.3969/j.issn.0258-2724.20190157

    RAO Chang, LI Nan, ZHANG Yadong, et al. Combinatorial test sequence set reduction approach for railway signaling safety-critical software[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 596-603. doi: 10.3969/j.issn.0258-2724.20190157
    [17] 吴彪. 基于EFSM的测试用例自动生成方法的研究[D]. 杭州: 浙江理工大学, 2016.
    [18] 石佳. 基于CBTC的联锁系统进路控制形式化建模与验证[D]. 成都: 西南交通大学, 2016.
  • 期刊类型引用(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)

  • 加载中
图(7) / 表(3)
计量
  • 文章访问数:  317
  • HTML全文浏览量:  164
  • PDF下载量:  17
  • 被引次数: 16
出版历程
  • 收稿日期:  2020-08-12
  • 修回日期:  2021-01-21
  • 刊出日期:  2021-04-01

目录

/

返回文章
返回