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

摘要：针对已有方法难以定量给出产品加速退化试验(ADT)结果可信程度的问题,以正常应力下的试验数据为基准,基于面积度量思想提出了一种加速退化试验结果可信性的定量评价方法。基于加速退化试验数据和基准数据的概率分布距离,构建了加速退化试验可信性的面积度量指标,在此基础上,提出了一种归一化、无量纲的加速退化试验可信度指标CIA,并基于时间重要度的概念将多个单点的CIA综合成一个可反映整个产品加速退化试验可信性的指标。实例分析表明,新指标可以让设计师和决策者直观评判产品加速退化试验结果的可信程度,方便横向对比不同产品的加速退化试验结果的优劣;所建立的新指标适用于基准数据大样本、小样本、极小样本等不同情况,具有良好的通用性。

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

摘要：检查强制文字是一种重要的预处理方法。结合学习子句,提出一种在求解过程中使用的策略—基于子句的动态检查强制文字(CNL),并且设计了一种易实现低成本的数据结构。分别实现了两个不同版本的求解器:Glucose_PRE和Glucose_CNL,前者在求解初始时将检查强制文字作为预处理,后者实现了基于子句的动态检查强制文字策略。实验测试结果表明,与Glucose_PRE和Glucose3.0求解器相比,求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时,求解实例个数更多,耗时更少,说明所提策略和所设计的数据结构均可提高求解器的求解性能。

摘要：基于不同分配策略的云计算任务调度以及任务分配与调度的主要目的,提出了一种新的算法—求解3-SAT问题的基于任务分配与调度的GSAT算法。该算法将3-SAT问题中的每一个变量形成一个任务,在GSAT算法的基础上,引入任务分配与调度指导贪心搜索;同时,在保留原有贪心搜索的前提下,根据任务分配与调度的思想和3-SAT问题的特点,设计了两种新的策略—分配策略和调度策略共同完成整个贪心搜索过程。以标准的SATLAB库中变量个数从20~250的3 700个不同规模的标准Uniform Random-3-SAT问题对新的算法的性能进行了合理的测试,并与高效和普通性能改进的GSAT算法的结果作了比较,结果表明,该算法具有更高的成功率和更少的翻转次数。

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

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