安全苛求系统的形式化开发方法

从系统工程的角度出发,基于形式化理论,对安全苛求系统的开发方法进行了研究.首先介绍了安全苛求系统的形式化方法,分析了形式化方法对安全苛求系统的作用;提出了一种安全苛求系统的形式化开发模型(FDM),给出了具体的应用实例.

安全性苛求系统中关于软件安全性评价的研究

安全性苛求系统由于其行为直接关系人身和大宗财产的安全 ,需要有一个安全性定量指标来反映系统中计算机软件的安全性品质。由于安全性苛求系统的软件在开发时规定要采取一系列可靠性和安全性措施 ,到形成产品后 ,软件内部缺陷的暴露都是一些小概率事件 ,如果仅仅依靠测试数据进行安全性定量评估 ,由于测试开销的限制 ,依据似感不足。本文提出一种多元、多模型、多阶段进行安全性评价的方法。在系统开发和运用的不同阶段 ,从不同角度 ,利用历史的和当前的数据 ,依靠客观和主观的判断 ,对系统的安全性进行评价 。

基于XML的安全苛求系统测试脚本生成

针对安全苛求系统(SCS)自动化测试中测试脚本规模大、结构复杂、难维护以及安全性测试需求的特点,提出一种基于XML的测试脚本自动生成方法。将XML作为测试脚本语言,使用SED模式设计SCS测试场景,采用FSM对SCS运营场景建模,设计一系列转换生成算法自动生成XML测试脚本,实现了SCS测试脚本自动化生成和验证,并成功应用到高速铁路CTCS-2级列车运行控制系统仿真测试中。

基于改进DFTA的安全苛求系统可靠性分析

针对传统可靠性分析方法容易忽视冗余多态性、可修复性等安全苛求系统特性问题,在形式化的系统可靠性建模中引入可修复因子,提出一种模块化动态故障树分析方法。在动态和静态相结合的模块化定量分析过程中,利用马尔可夫模型和顶事件发生概率逼近算法,有效避免动态故障树分析过程中的状态组合爆炸问题,提高安全苛求系统可靠性分析的可行性和实践效率。

基于模糊逻辑的安全苛求系统失效模式与影响分析研究

针对传统RPN(风险优先数)方法在安全苛求系统FEMA(失效模式与影响分析)过程中的不足,提出一种基于FRPN(模糊风险优先数)的新方案,即运用模糊逻辑理论进行定量的FMEA。通过运用模糊加权几何平均计算失效模式的FRPN,据此对失效模式的风险程度排序,寻找影响系统安全性的主要因素,并将其作为改善对象。最后将该方法应用到高速铁路列控系统的FMEA过程中,结果表明,所提出的FRPN方法比传统RPN更加科学严谨,更能紧密联系应用环境,具有较高的科学性和实用价值。

安全苛求系统综合功能危险源分析方法的研究

基于经典方法改进的安全分析方法—综合功能危险源分析(IFHA),综合了功能故障分析(FHA)、故障模式及影响分析(FMEA)、瞬时故障和可操作性研究(HAZOP)以及故障树分析(FTA)的分析原理,通过不同分析阶段结果的关联以及统一的故障树表示,保证系统分析全过程的一致性,克服了分别使用经典分析方法所出现的问题以及矛盾。IFHA应用于CBTC的地面子系统—ZC系统,帮助识别在系统设计阶段ZC软件功能可能出现的危险源,此例既可作为一个案例也可作为继续分析的项目。将ZC系统的软件和硬件结合进行的安全分析将是下一步的分析工作。

安全苛求系统下的嵌入式C语言程序调试技巧

介绍安全苛求系统下的嵌入式C语言程序调试的技巧。总结安全苛求系统的编码和程序调试工作中的嵌入式C语言调试经验,介绍正式代码调试之前的3件准备工作,代码调试的"版本升级比较法",打印添加技巧以及其它调试技巧和经验。

模型驱动开发在安全苛求系统中的应用

主要探讨了安全苛求系统在新需求下,如何在提高软件功能安全性的同时保证软件的质量和可信性。首先分析了在典型领域内安全苛求系统开发的标准流程,然后提出了基于模型驱动开发(MDD)SCADE(安全苛求应用开发环境)工具的开发流程。目的是规范和指导领域内安全苛求系统中的MDD开发,最终可以实现降低软件开发成本、提高软件交付质量和确保软件安全性的目的。

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

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

轨道交通信号系统安全技术的发展和研究现状

轨道交通系统作为大容量公共交通工具,其安全性直接关系到广大乘客的生命安全,信号系统作为保证列车安全、正点、快捷、舒适、高密度不间断运行的重要技术装备在轨道交通系统中有着举足轻重的地位。随着计算机技术在轨道交通信号系统中的应用,原有的安全保障技术和方法已不能满足越来越高的安全要求。为了使相关研究人员了解和应用国外信号系统的安全技术方法,笔者从科学技术发展的角度探讨了信号系统安全技术和专业术语的历史演变,对于一些重要的术语进行了比较和解释;从国外最新的相关研究成果和安全标准来看,在系统开发之前需要进行系统的前期安全评估,对于潜在的危险和故障进行分析和记录,作为研发过程中主要解决的安全问题;关于安全技术和意识问题应当贯穿于信号系统设计、开发、生产、装备、维护过程中,而不是等到系统研发出来之后再考虑安全问题。

列车运行控制系统设计正确性的验证方法

为验证系统开发阶段列车运行控制系统设计的正确性,提出了基于RAISE软件的系统建模、描述及验证方法.以CTCS-3级两列列车追踪运行为例,采用面向系统特性的域,建立了系统域模型,并在对域模型扩充和完善的基础上,用RSL语言描述了两列列车追踪运行情况.根据RSL语言描述的公理及RAISE自身的推理规则,验证了当两列列车追踪运行时,CTCS-3级列车运行控制系统设计的正确性.

联锁系统形式化模型的安全性评估

根据联锁系统的事故危害度分类,有效地结合故障树分析法和Petri网可达图分析的各自优点,提出一种用于评估联锁系统Petri模型的安全性的方法,并通过实例验证其有效性。

基于场景分析的系统形式化模型生成方法

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。

面向安全评估的CTCS-2列控系统安全性测试环境

高速铁路CTCS-2列控系统是典型的安全苛求系统。根据安全苛求系统的特点,针对高速铁路CTCS-2列控系统的安全性测试和评估需求,设计了场景—事件驱动的测试脚本语言SED_TSL,提出了高速铁路CTCS-2列控系统测试环境的功能、系统框架、测试策略,实现了基于SED_TSL的CTCS-2列控系统自动化测试环境,并投入到铁道部的CTCS-2列控系统产品制式检测中,有效地实现了列控系统产品的功能与安全性测试。

列车运行控制系统安全保障与认证方法研究

为了保证轨道交通系统的运行安全性,系统必须在其投入运行之前进行安全认证,只有取得相应的安全授权才能投入运行。结合CENELEC国际标准和我国应用实践,提出以安全验证和确认为基础的安全保障与认证方法,将安全验证和确认的方法贯穿于系统研制开发生命周期内的每一个阶段,监控系统研制开发的每一个活动,评审系统研制开发的每一个文档,保证相关文档之间的追溯性,针对系统的所有需求进行完备性和充分性测试,才能够确保列车运行控制系统能安全、可靠地投入使用。列车运行控制系统是轨道交通系统的重要组成部分,关系其运行安全和效率2,010年底采用安全验证和确认的方法成功地将LCF-300型列车运行控制系统应用于北京轨道交通亦庄线和昌平线,并顺利通过英国劳氏公司的第三方安全认证。

一种基于COTS硬件的安全苛求计算平台研究

为解决安全关键领域传统容错计算平台支持费用高、技术局限性大的问题,提出并实现了一种基于商用货架产品(COTS)的高安全容错计算平台(VIS),给出了平台的构造方法,分析了VIS平台的2 oo2×2体系结构和容错同步原理.遵循IEC 61508标准对平台进行了安全完整性等级确认.结果表明,VIS平台的硬件安全完整性达到SIL4级,能够满足安全苛求领域的需求.

基于UPPAAL的列车自动防护系统形式化建模与验证

本文分析列车自动防护(ATP)系统的结构和功能需求,建立系统的时间自动机模型,采用UPPAAL模型验证工具对模型的活性和安全性进行验证。结果表明,采用时间自动机对安全苛求实时系统进行建模与验证,可以有效地保证系统的可靠性和实时性。

基于UPPAAL的列控系统临时限速建模与验证

临时限速系统是列控系统的重要组成部分,是符合"故障–安全"准则的安全苛求系统。文章基于临时限速技术规范和时间自动机理论,分析临时限速系统的组成结构,提取其功能和性能约束,利用UPPAAL工具对其信息交互行为进行建模仿真,验证该系统的实时性,为进一步完善临时限速系统的设计与开发提供参考。

CBTC系统数据管理过程分析和设计

阐述基于通信的列车自动控制(CBTC)系统的功能,讨论其系统数据所具有的空间性、一致性和关联性等特点。针对CBTC系统数据的特点,提出一种基于数据供应链(data supply chain,DSC)对数据管理过程进行分析和设计的方法,给出具体设计过程的7个步骤,并讨论该方法的可用性和可行性。

苛求软件可靠性方法、技术与模型研究

从瀑布式程序设计的角度,综述了苛求系统软件生命周期各阶段的可靠性方法、技术和模型,包括需求形式化建模与验证、屏蔽设计错误的多版本软件容错、函数式程序设计以及可靠度评估模型等。总结比较各自适用的开发阶段、面向的目标错误类型及优缺点。