基于形式化方法的平交道口控制系统安全设计

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.

基于近期文字极性分配的学习子句评估算法

为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句有用性的方法,从而保留对求解最有促进作用的学习子句,以提高求解效能。从捕获学习子句近期的极性分配出发,结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省,来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准,针对其在子句评估环节的算法进行改进测试。实验结果表明,这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率,有效改善了原有求解器在一些问题上求解耗时过长的问题,并在先进求解器的水平上多求解了2个合取范式CNF文件,单个文件的平均求解时间缩短了13~34 s。

基于知识图谱和故障树的高速铁路事故致因分析

针对高速铁路(简称:高铁)事故开放共享程度不高,数据条块化、垂直化,信息碎片化等问题,基于知识图谱构建高铁事故的本体层及数据层,实现事故数据的资源整合,使用图数据库表达事故致因逻辑关系,通过Python编程生成高铁事故致因故障树,完成对高铁事故的致因分析。分析结果表明,人为因素中的“违规作业”“监管不力”及环境因素中的“恶劣天气”导致了更多高铁事故的发生。据此结果,为铁路相关部门防范重大事故发生提出了切实可行的建议。

突发事件应急血液调剂问题的两阶段决策方法

基于血液的生理特性及应急保障特性,以应急血液最晚运达时间最小、接收时的最低新鲜度最大、运输总费用最小为目标,建立考虑多品种、多式联运的应急血液调剂出救点选择,即运输路线安排问题两阶段决策优化模型,并设计了一种包含局部邻域优化的遗传,即禁忌混合算法进行求解.以"5.12"汶川大地震应急血液保障为背景构建算例,分析验证了两阶段决策方法在最晚抵达时间、新鲜度均值、运输总费用、血液积压量等指标上的优越性.

灾后重建地区新增血站的选址问题研究

根据灾后重建地区血液保障体系建设的实际情况,考虑血站间的依附系数对血站布局的影响,建立了一种p-中值模型用来解决新增血站的选址问题,并设计了一种遗传-禁忌混合算法对模型进行求解。之后以汶川大地震灾区——四川省阿坝州为例进行了实例分析,得到了不同p值与依附系数下的新增血站选址方案,以期为相关部门规划灾后重建地区的血液保障体系提供理论依据与决策参考。

水平穿越理论在库存控制研究中的应用

库存控制一直是工业工程研究领域关注的焦点之一。水平穿越理论巧妙地建立起了库存系统中入库、需求、在库物品库龄等变量之间的联系,为复杂随机系统状态属性的动态性分析提供了一种新的理论工具。以M/G/1队列为例引出了水平穿越理论的基本原理,通过虚拟到期过程分析系统点的变化建立其在易腐品库存控制中的应用模型,并基于恒定变质率的易逝品库存模型推导了其在普通物品库存控制中的应用过程。按照入库、需求、提前期等变量表现形式的不同,文对该方法在库存控制研究中的应用进行了系统性的回顾,最后指出了进一步的研究方向。

中国高铁联调联试与运行试验现状分析

介绍了高铁联调联试与运行试验的作用和内容。对联调联试与运行试验过程中存在的进行时间紧凑、缺少其他相关部门的参与、人员演练需要加强、缺少独立第三方的安全评估等现状问题进行分析,提出了组织计划统筹、测试案例库构建、系统状态评价等需深入研究的要点,并建议进行全生命周期的RAMS(可靠性、可用性、可维护性和安全性)评价,为我国高铁联调联试与运行试验体系的进一步完善提供参考。

车站联锁系统行为验证与数据确认的形式化方法

车站联锁系统是一种典型的基于数据驱动的安全苛求系统,开发过程中需要对系统行为进行验证并需确认数据的正确性.为此,通过分析联锁系统的设计规范,基于RODIN平台并使用Event-B语言,辅助使用UML(unified modeling language)图工具快速建立系统的初始模型,以自动生成模型文件并描述出各系统属性与事件流程;基于精化策略分层建模,对各层模型的证明义务进行定理证明,验证了系统的各项属性,得出可靠的通用功能模型;基于实例车站,对模型的公理进行了验证,同时实现了对联锁数据的确认;通过形式化验证过程,结合给定场景联锁数据的有效性确认,发现并纠正系统需求及分析过程中造成的潜在行为缺陷;通过功能仿真与验收测试,进一步确认了通用模型与联锁数据的正确性.结果表明:本文方法提高了基于模型开发过程的准确性与层次性,验证了系统通用行为状态,且结合公理验证,实现了联锁数据的确认,并能基于模型进行功能场景仿真与测试,从而可进一步提高系统通用功能原型的可靠性.

基于累积前景理论的随机异质道路网配流模型

针对出行者择路行为的有限理性和风险取向的差异性,将出行者分为4类:分别以可靠度低于50%的出行时间预算、期望出行时间、可靠度高于50%的出行时间预算和超预算期望出行时间作为选择路径的参考点.推导了需求服从对数正态分布、路段通行能力服从均匀分布条件下各类出行者的前景值计算公式,建立了用等价变分不等式表示的均衡模型.算例结果表明,累积前景理论参数设置对配流具有重要影响,随着收益敏感系数的增大,各类出行者的路径前景均呈增大趋势,且第3、4类出行者比第1、2类出行者变化更显著;随着损失敏感系数和损失规避系数的增大,各类出行者的路径前景均呈减少趋势,且第1、2类出行者比第3、4类出行者变化更显著;随着感知概率系数的增大,第1、2类出行者的路径前景呈减小趋势,而第3、4类出行者的路径前景呈增大趋势.

有容量限制的可靠性固定费用选址问题

设施网络可能面临各种失灵风险,而设施选址属于战略决策问题,短期内难以改变,因而在选址设计时需要充分考虑设施的非完全可靠性。本文针对无容量限制的可靠性固定费用选址问题进行扩展,进一步考虑设施的容量约束,基于非线性混合整数规划方法建立了一个有容量限制的可靠性固定费用选址问题优化模型。针对该模型的特点,应用线性化技术进行模型转化,并设计了一种拉格朗日松弛算法予以求解。通过多组算例分析,验证了算法的性能。算例分析结果表明设施失灵风险和设施容量对于选址决策有显著影响,因而在实际的选址决策过程中有必要充分考虑设施的失灵风险及容量约束。

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

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

基于B方法的轨道交通控制系统配置数据的形式化验证

轨道交通控制系统对安全性和可靠性要求极高,其正常运行依赖于正确的配置数据,因而采用有效的方法保证配置数据的正确性显得十分重要。以轨道交通控制系统的配置数据为研究对象,选取道岔、信号机、轨道区段、进路等站场型信号设备数据为研究案例,基于各个配置数据的站场型数据结构,先用自然语言描述各个配置数据和配置数据需要满足的静态规则,再使用B语言形式规约各个配置数据及其所需要满足的静态规则,建立静态形式化模型,最后使用ProB模型检验工具,验证分析已生成的各个配置数据是否满足静态规则。验证结果表明,使用B方法对轨道交通控制系统配置数据进行形式化验证,有效提高配置数据正确性,进而为轨道交通控制系统的正常运行提供可靠保障。

基于B方法的道岔控制系统形式化建模与验证

为解决目前安全苛求系统研发中的功能安全问题,以用于轨旁设备联锁控制的道岔控制系统为研究对象,基于系统需求规范,使用形式化软件开发方法(B方法)对系统的功能逻辑建立形式化模型,完成对需求规范、系统功能及决策过程的验证,最终生成C语言形式的可执行代码。在分析系统各类属性与联锁逻辑关系的基础上,使用一阶逻辑和公理化集合论的数学方式,严格定义系统各层的B语言模型。通过对不变式的证明义务进行证明,验证系统中的安全、时间特性,检查出需求规范中的缺陷,提出增强系统稳健性的改进方案,进一步修正系统设计原型。通过不变式冲突和死锁检验进一步确认系统的正确性。研究表明,在所有证明义务通过机器自动证明和手动交互式证明的验证后,B模型自动生成的C代码能够正常运行并且功能满足实际联锁需求。将形式化方法应用于系统开发的全过程,所使用的技术路线及开发方法可以有效提高道岔控制系统的安全可靠性,并减少编码阶段工作量,对其他安全苛求系统的开发有重要参考意义。

数据硬件读写方案在TMIS中的实现研究

针对TMIS中数据难以用第三方软件方式交互式访问的现状,本文提出了用硬件方式实现数据的读取与写入,避开在软件方法上开发资料不全、数据库须与操作系统接口统一等难题。文中讨论了方案的实现过程,并给出基于并行总线获取数据、通过PS/2总线模拟键盘输入的硬件电路与实现过程。

基于网络连接及服务中心选择的高铁路网区域划分方法

高速铁路路网的区域划分对于区域性运行图的编制具有重要意义。结合路网的邻接特性,并考虑动车储备与检修能力进行区域中心的选择,以区域内的最小连接距离、最大平均连接紧密度为目标,建立高铁路网区域划分混合整数规划模型,并设计向量编码方式的遗传优化求解算法、高铁客运周转量折算方法。最后,以中国铁路总公司所属路网区域构建算例,对比聚类算法说明文中模型与算法的有效性与适应性,分析目标函数权重系数、最大服务半径与最大服务容量约束对划分结果的影响,得出服务半径系数、服务容量系数的设定方法。

应急救援中积压血液的转运

为应对因突发事件造成大量人员伤亡而引起的用血量增长,血站往往过量增加库存以至造成血制品积压,因此必须及时转运积压血液制品以减小潜在的过期报废。通过分析库存状态,基于库龄推导出血液转运、接收的相关性质,建立最小化运输费用的转运模型;最后通过算例仿真验证了不同转运制品选择策略的差异以及保障概率、需求饱和度对使用新鲜度的调节作用,并分析了决策时刻对决策效果的影响,为应急保障中积压血液的转运决策问题提供了理论依据与实例参考。

应急血液多阶段调剂优化

血液是一类特殊的应急物资,在灾害救援中发挥着至关重要的作用.为提高应急血液保障效率,通过分析血液特性与应急血液保障的阶段性特点,并考虑运输方式对血液质量的影响,建立了一种多阶段优化模型解决多灾点、多品种应急血液调剂问题,设计了一种基于关键受灾点优先的向量编码遗传算法进行求解,并对算法的时间复杂性进行了分析.最后,以汶川大地震应急血液保障为背景构建算例进行验证,结果表明该遗传算法的计算效率较高,所提的多阶段决策方法在血液新鲜度、血液积压量等方面具有明显优势.

应急物资储备库的可靠性P-中位选址模型

应急物资储备库选址属于战略性决策问题,而突发事件的发生可能会造成储备库失灵,因此在选址设计阶段就考虑其失灵风险是十分必要的。本文以应急物资保障的及时性和可靠性为目标,考虑在不同地区建立储备库的不同失灵概率,建立了一种应急物资储备库的可靠性P-中位选址模型。针对该模型的特点,运用线性化技术进行模型转化,并设计了一种拉格朗日松弛(LR)算法。最后通过两组算例分析对模型和算法进行验证,并与CPLEX求解结果进行了比较。结果表明,对于大规模问题,LR算法效率明显高于CPLEX。

基于卫星云图的风矢场度量模型与自适应算法

探讨了基于卫星云图度量风矢的模型与算法.首先,构建三维地球坐标系和二维帧平面坐标,实现了经纬度与灰度矩阵的行列号的相互转换;其次,近似修正定位目标云,采用最大交叉相关系数选择最优化匹配云,进而建立固定尺度下风矢度量模型;再其次,根据该先验信息构造变尺度的搜索空间,设计自适应算法加快搜索进程和提高精度;最后,挖掘预报文件中的温度-压强关系,分段拟合风矢的压强和所在等压面层数.

道口管理系统多参数的形式化建模与验证

铁路平交道口作为铁路安全的瓶颈,其作业流程的缺陷是导致安全事故发生的重要原因之一。而现有道口管理规范大部分只针对单线接车,对于双线双向接车没有给出详细的规范。为了丰富实际流程,基于道口管理规范,探讨双线双向道口连续接车的问题,同时考虑道口接车作业流程中存在的异常,提出流程方案。分析系统环境属性、功能属性和安全属性,并利用UPPAAL时间自动机进行建模仿真,对模型的属性进行验证,根据验证结果确认方案流程的可行性。结果表明,本文所提出的多参数道口作业流程更符合实际情况,改进了多列车接车流程,并提出了接车过程中异常情况下的应对方案。