关键性安全系统安全完整性概述

介绍关键性安全系统的安全与风险基本概念、安全完整性的实现,以及功能安全要求标准IEC61508：2010的结构、功能安全的要求与实现、安全完整性评估。     

Design of software for safety critical systems

In this paper, we provide an overview of the use of formal methods in the development of safety critical systems and the notion ofsafety in the context. Our attempt would be to draw lessons from the various research efforts that have gone in towards the development of robust/reliable software for safety-critical systems. In the context of India leaping into hi-tech areas, we argue for the need of a thrust in the development of quality software and also discuss the steps to be initiated towards such a goal. “If only we could learn the right lessons from the successes of the past, we would not need to learn from our failures” C.A.R. Hoare An earlier version was presented as an Invited paper at the ISRO Conference on Software Engineering, VSSC, Trivandrum, 29–30 July 1994.     

Design and Test of a Certifiable ASIC for a Safety-Critical Gas Burner Control System

The purpose of this paper is to present a methodology and tools for the design and test of an EN298 compliant ASIC chip for a safety-critical gas burner control system. Safe operation, as far as the critical variable is concerned, is guaranteed in the presence of two simultaneous faults. Emphasis is put on circumventing methodology, EDA (Electronic Design Automation) and foundry limitations and on product certification requirements.     

实时系统的虚拟内存技术

本文对实时系统的虚拟内存技术作了深入的分析和讨论，并以X86处理器为例．在嵌入式操作系统CRTOSII上完成了一个内存管理系统的详细设计与实现。     

Building Large,Complex, Distributed Safety-Critical Operating Systems

Safety-critical systems typically operate in unpredictable environments. Requirements for safety and reliability are in conflict with those for real-time responsiveness. Due to unpredictable environmental needs there is no static trade-off between measures to accommodate the conflicting objectives. Instead every feature or operating system service has to be adaptive. Finally, for any design problem, there cannot be any closed-form (formal) approach taking care at the same time of (external) time constraints or deadlines, and synchronization requirements in distributed design. The reason is that these two aspects are causally independent. - In this situation we worked out a heuristic experimental, performance-driven and performance-based methodology that allows in an educated way to start with a coarse system model, with accurate logical expectations regarding its behavior. Through experiments these expectations are validated. If they are found to successfully stand the tests extended expectations and model features are generated for refining the previous design as well as its performance criteria. The refinement is done in such a way that the previous experimental configurations are extreme model cases or data profiles which both logically and experimentally are to reproduce the behavior of the previous modeling step. Thus the novel performance aspects or tendencies could then unambiguously be attributed to the influences of the refined model features. We termed this methodology Incremental Experimentation. As a general methodology it relies on a principle of comparative performance studies rather than on realistic data for narrow application ranges. The paper describes how we applied a 5-step design and refinement procedure for developing, analyzing, and evaluating our distributed operating system MELODY that exhibits novel services for supporting real-time and safety-critical applications in unpredictable environments. Experimental set-ups and theme-related findings are discussed in particular.     

自适应防危策略的设计技术研究

当安全关键系统中的某些环境发生变化时,其对应于某些关键设备的防危策略也会皆然不同。本文以核电站控制系统为原型,提出一种基于有限制动机,利用自适应中间件QuO(Quality Objects)实现的自适应防危策略。该策略可以用于不同类型设备的其他安全关键系统中。     

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

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

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.     

一种SysML模型到AADL模型的自动转换方法

安全关键系统的实现需要通过需求、设计、集成、验证和测试等多个阶段。近年来,模型驱动开发方法逐渐成为安全关键系统设计与开发的重要手段。由于还没有一个建模语言能够支持整个安全关键系统开发生命周期,因此选择集成使用2种广泛使用的标准语言:系统建模语言(SysML)和嵌入式实时系统体系结构分析与设计语言(AADL)。SysML和AADL提供了同一系统的2个不同视图,SysML模型为系统工程师提供了一个系统视图,AADL为架构设计师建立一个较低层次的设计视图,它结合了实现所有功能的硬件、操作系统和代码。提出一种SysML模型到AADL模型的自动转换方法。首先,定义SysML子集SubSysML,主要包括模块定义图(BDD)、内部模块图(IBD)、活动图(ACT)子集和从IBD和BDD扩展的AADL Profile;其次,定义SubSysML到AADL的转换规则并设计转换算法;然后,对生成的AADL初始模型进行精化;最后,使用EMF框架技术实现SubSysML到AADL的模型转换工具并通过雷达案例验证所提方法的有效性。     

AltaRica 3.0模型到Promela模型转换与验证方法研究

AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力方面的改进,以及其底层模型GTS的基本结构。以AltaRica3.0扁平化为GTS模型的思想为基础,提出了一种AltaRica3.0模型向Promela模型的转换规则。以民用飞机中机轮刹车系统WBS为例,建立了AltaRica3.0模型,并且通过转换规则转为Promela模型。最后根据民用航空标准SAE ARP 4761中对机轮刹车系统的安全性要求,利用SPIN工具对机轮刹车系统的安全属性进行了验证。