高铁信号系统安全关键功能测试建模方法

测试模型是高铁信号系统安全关键功能测试用例编制的重要基础,针对高铁信号系统安全关键功能测试建模过程中描述信号系统领域特征不够全面的问题,提出时间状态机测试建模理论和测试用例生成方法. 分析高铁信号系统测试建模的特点,提出信号系统安全关键功能测试模型的建模需求;以有限状态机理论为研究基础,结合功能逻辑和时钟约束提出时间状态机建模方法,采用Z规格说明语言给出时间状态机的形式化定义;将时间状态机转换为时间自动机,证明转换之间的一致性,并基于时间自动机的测试理论自动生成测试用例,再以计算机联锁系统中的道岔转换功能为例,建立时间状态机测试模型并生成测试用例. 最后,将两种方法生成的测试案例进行对比,结果表明:在功能逻辑方面,基于时间状态机建模方法生成的测试案例100% 地覆盖了基于时间自动机建模方法生成的测试案例,并新增了16条具有时钟约束的测试案例,能够满足高铁信号系统安全关键功能测试建模的需求.      

基于TSSM的城市轨道交通CBTC区域控制器建模与验证

针对安全状态机缺乏时间描述能力的缺点,利用反应式系统的同步设计方法,提出了时间安全状态机TSSM (timed safe state machine)建模方法,定义了弱变迁和同步变迁语法,建立了城市轨道交通ZC (zone controller)系统模型.首先,分析了ZC系统的运行环境、工作原理和功能需求,根据ZC反应式系统的特点,利用TSSM在SCADE (safety critical application development environment)中建立了ZC系统列车管理、ZC控制、MA计算和队列管理子模型;其次,通过ZC系统的TSSM网络模型,分析了子模型间的交互信息;最后,采用Lustre语言对ZC系统的安全特性进行了形式化描述,并利用Design Verifier模型检测工具,结合数据流验证了ZC系统的功能和性能需要.研究结果表明,ZC系统TSSM模型的安全性和受限活性均为有效,ZC系统完全满足预期的安全需求.      

铁路信号系统风险严重度综合评判

为更科学地评估铁路信号系统的风险严重度,根据铁路信号系统的特点,在专家打分法的基础上,综合应用层次分析法、加权平均型综合函数和最大隶属度原则,提出了铁路信号系统风险严重度综合评判方法.以微机化自动站间闭塞系统为例,分析了系统延时建立闭塞的风险严重度,并对其进行了综合评判.     

基于模型的CTCS-3级列控系统测试案例自动生成方法

为了提高CTCS-3级列控系统测试案例生成效率,提出了基于混合通信顺序进程(hybrid communication sequential process, HCSP)形式化模型和时间自动机(timed automaton, TA)形式化模型的列控系统测试案例自动生成方法;建立了列控系统运营场景的时序模型,分析了列控系统运营场景规范中时序功能的正确性;在时序模型的基础上,设计了满足全状态、全变迁和自定义-使用3种领域无关覆盖准则的列控系统测试案例自动生成算法,并以RBC(radio block center, RBC)切换场景为例,生成了100%全状态、全变迁和自定义-使用覆盖准则的测试案例套.从测试套数量、测试时间和内存消耗3个方面分析测试案例的生成效率表明:自定义-使用覆盖准则的测试案例套测试时间和内存消耗最小,分别为0.02 s和9.4 MB,本文方法提高列控系统测试案例生成效率最大达30%.      

一种基于有限自动机的软件开发模型

结合工业控制领域中的实际情况,提出了一种基于有限自动机的软件开发模型。该模型利用有限自动机的理论,将单个工业设备的行为映射为自动机的状态变迁,当工控设备更新后,用户只需开发相应的子服务组件或模块,便可进行系统扩充乃至系统重构。     

����ɫPetri����������ͨ�ŵ� �г� ����ϵͳ�IJ��ģ��

基于通信的列车控制系统是我国铁路信号技术发展的一个重要方向，本文在分析了基于通信的列车控制系统结构的基础上，采用有色Petri网方法对该系统进行建模仿真研究.有色Petri网是一种以图形形式描述系统结构、功能的建模分析方法，特别适合大型异步并发系统的建模与仿真.为了使模型简洁清楚，提出了分整体层、处理层和功能层三部分建立相应的系统有色Petri网图的分析方法，并用CPN /Tools工具软件来实现.通过建立一个墓于通信的列车控制系统的有色Petri网模型，为最终开发出该系统的软件仿真平台莫定了良好的基拙.     

CTCS-3级列控系统临时限速建模与验证

为了满足临时限速系统的实时性要求,采用时间自动机理论,对CTCS-3级列控系统临时限速工作流程分别建立了各设备的时间自动机子模型,进而构成临时限速系统的时间自动机网络模型,并基于临时限速系统技术规范的参数对模型进行赋值;采用BNF语法对临时限速系统待验证的属性进行了形式化描述,并应用UPPAAL验证工具对临时限速模型的安全性和受限活性进行仿真验证.验证结果表明:与现有临时限速系统的时间参数设置相比,修正后的时间参数设置避免了出现系统死锁现象;在不影响安全功能属性和受限活性的基础上,提高了临时限速系统的实时性,可在规范规定时间5 s内做出响应.      

中国铁路信号系统智能监测技术

介绍了中国铁路信号监测技术现状,结合国外监测技术发展趋势和铁路信号系统维护需求,在分析我国铁路信号监测系统在互联互通、数据共享、智能分析与预测等方面不足的基础上,提出了建立综合智能化电务监测维护系统的构想,并给出了系统总体架构.阐述了系统的分层功能和所涉及的共享数据甄选、数据集成模式、智能分析、接口规范等关键技术,为实现电务设备由“故障修”到“状态修”的综合智能维护提供了可行途径.最后,讨论了系统构建过程中分层分步和兼顾现状的实施原则,指出了监测系统与信号系统间信息安全等级划分等需要注意的问题.      

基于UML的C3I仿真测试环境建模研究

建模技术在复杂软件系统的设计、开发、集成和测试中起着重要的作用．C^3I仿真测试环境所面临的问题是如何准确、有效地描述系统元素间的交互并快速建立系统原型模型．文中从UML的需求、结构、行为和实现模型来描述C^3I仿真测试环境的基本结构、组成元素、系统和对象间的交互以及从模型到具体设计的实现，从而完成基于UML的C^3I仿真测试环境的系统建模过程．该建模方法已在某测试环境中实现，缩短了系统的开发时间并确保了系统的性能和可靠性．     

时间自动机的自动抽象算法

为对付时间自动机规格分析验证中的状态爆炸问题，提出了一种自动抽象算法．它是直接在时间自动机描述规格上而不是在规模大得多的语义模型上进行抽象，从而取得不大于时间自动机拓扑复杂性的四次方的多项式复杂度，实验证明，该算法可应用于任何满足线性复位性质的时间自动机。此外，这种算法还可以用来简化系统描述，提高其可理解性。     

基于威胁分析的高速铁路信号系统风险评估方法

高速铁路信号系统是实现列车安全运行的关键基础设施，一旦发生设备或系统功能性故障极易导致安全事故. 为此，提出了一种功能安全视角下用于高速铁路信号系统风险评估的模糊综合评价方法. 该方法在改进模糊综合评判和层次分析法（analytic hierarchy process，AHP）的基础上，加强系统威胁场景分析，并建立各场景下风险因素耦合关系. 首先，分析高速铁路信号系统中影响行车安全的5类44个威胁场景，以系统功能安全事故为分析准则层、威胁类别为因素层，构建递阶层次结构；然后，根据主观评价确定结构中各要素权重，结合评语集对风险进行综合评估，并根据各场景风险值变化动态调整各层级和因素的权重，使评估结果更为真实，且能在安全风险和信号业务间建立映射关系. 最后，通过评估某客专真实安全数据，得到信号系统风险等级较低的结果，与其他方法测评结果基本一致，验证了该方法的有效性.      

站间微机化自动闭塞系统双机冗余系统设计

根据站间自动闭塞系统的高可靠性要求，设计了闭塞机热备冗余方案；针对可能出现的双主机状态，研究了安全控制锁的原理与机制．为了解系统的转换性能，用Petri网对系统进行了建模与分析．分析结果表明，设计的结构与切换机制合理，系统中各状态转换安全、完整，不存在死锁状态．     

Software Testing Method Based on Model Comparison

A model comparison based software testing method (MCST) is proposed. In this method, the requirements and programs of software under test are transformed into the ones in the same form, and described by the same model describe language (MDL).Then, the requirements are transformed into a specification model and the programs into an implementation model. Thus, the elements and structures of the two models are compared, and the differences between them are obtained. Based on the diffrences, a test suite is generated. Different MDLs can be chosen for the software under test. The usages of two classical MDLs in MCST, the equivalence classes model and the extended finite state machine (EFSM) model, are described with example applications. The results show that the test suites generated by MCST are more efficient and smaller than some other testing methods, such as the path-coverage testing method, the object state diagram testing method, etc.     

基于PLC控制技术的铁路起重机电气控制系统

对NS1251型伸缩臂式铁路救援起重机的运行动作进行分析,并根据其电液比例控制的要求设计了采用PLC逻辑控制器的电气控制系统,着重介绍了控制系统的硬件设计和软件设计原理和设计思路．在此基础上对所设计的电气控制系统的应用情况进行了介绍．实践证明采用这种电控技术改善和提高了NS1251铁路起重机的可靠性、可操作性、维修方便性等,综合性能大大地超越了全液压控制的铁路起重机的性能．     

基于TCPN的铁路客运站作业组合仿真模型

为解决现有铁路车站作业系统仿真模型建模过程复杂、适用范围有限、效率不高等问题,根据站场布置图,用进路冲突图描述车站列车进路及进路关系,并在此基础上建立了适用于不同站场布置图的赋时有色Petri网(timed colored Petri net, TCPN)仿真模型.车站作业过程仿真结果表明: TCPN仿真模型性能与结构稳定,适用于包括高速铁路在内的任意铁路客运站站型图的作业过程仿真及优化;冲突图模型与现实车站系统相似程度高,对车站布置图的描述精度与施工图精度相同,最高可达毫米级;与传统铁路车站仿真软件手工建模过程相比,冲突图模型建模效率高,建模过程耗时小于1 s;仿真过程咽喉进路最高负荷为70%,到发线最高负荷为35%,列车到达正点率100%,出发正点率91%.      

基于UKF的数字轨道地图的三维线路生成方法

针对基于卫星导航系统的列车定位对数字轨道地图的实际需求, 提出了一种基于无迹卡尔曼滤波的线路估计方法, 生成线路的三维数字轨道地图; 对于铁路线路的3种平面线形(直线、缓和曲线和圆曲线), 采用以里程为参数的菲涅尔(Fresnel)积分模型统一建模; 对于纵断面的直线和曲线, 采用二次曲线模型建模; 用无迹卡尔曼滤波对模型的状态(里程、三维坐标)和参数(方位角、曲率、曲率变化率、坡度、坡度变化率)进行联合估计; 将归一化新息平方和估计距离误差作为线路分段的判断条件, 最终用分段点和几何参数完成三维线路的生成; 采用仿真的平面线路数据对比了离散点法、三次多项式法和本文Fresnel法, 利用青藏线14.7 km的实测数据进一步对Fresnel法进行了验证。仿真结果表明: 在相同的误差要求下, 3种方法的平面距离误差均值都在0.024 m以内, 但Fresnel法采用了最少的分段点, 数据约简率高达99.76%; Fresnel法的最大累积里程误差最小, 由0.964 m降低为0.060 m, 减少了93.77%;Fresnel法比三次多项式法的方位角和曲率估计精度都高, 更加接近真值; 实际数据测试结果表明Fresnel法分别采用22个和20个分段点及参数即可完成线路的平面曲线和纵断面曲线生成, 平面和纵断面曲线距离误差均值都在0.03 m以内, 累积里程误差最大只有0.078 m, 位置精度和几何精度都较高。      

铁路缓和曲线代数式方程的通用设计方法

根据铁路缓和曲线的特点,介绍了利用缓和曲线边界条件确定其代数方程式的一种通用方法：首先给出缓和曲线要满足的边界条件,根据边界条件列出曲率待定方程;然后利用曲率边界条件确定出缓和曲线曲率方程;最后通过对曲率方程进行二次积分就可得到缓和曲线的方程。采用这种方法分别对各种类型的缓和曲线举出实例,详细说明了该方法的应用,证明了该方法正确、简单,是一种适用于推导缓和曲线方程的通用方法,可为铁路缓和曲线线型设计提供参考。