一种安全关键软件系统符号执行优化方法

在航空、核电和国防军工领域当中,安全关键系统(Safety-Critical System,SCS)的软件非常重要,其可靠性必须通过测试或形式化方法来保障。符号执行作为一种高效的测试用例生成方法被广泛使用,然而,SCS软件系统的模块之间的耦合性较高,使得符号执行约束求解困难。本文针对这类软件系统提出一种带权最小割集的解耦方法,为安全关键软件系统的自动化测试提供了一种新思路。     

支持SPIN验证的详细级SFMEA方法研究

随着软件系统的规模和复杂度不断增大,以软件为核心的安全关键系统的可靠性和安全性越来越难以保证。软件失效模式与影响分析SFMEA(Software Failure Modes and Effect Analysis)是军工业中常用的一种安全分析方法,其依赖人工分析、缺乏形式化语义、无法支持验证。针对SFMEA方法的不足,提出一种结合SPIN的详细级SFMEA方法,对软件失效模式进行形式化建模与分析,并结合模型检验工具SPIN进行自动化地模型检验和模拟仿真,从而提高软件系统的安全性和可靠性。该方法验证了"缓冲区数组下标越界"的这一失效模式,从而说明该方法的有效性。     

一种结合线性时序逻辑和故障树的软件安全验证方法

嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线性时序逻辑和故障树的安全验证方法。该方法运用线性时序逻辑对故障树进行形式化规约,从中抽取出软件安全属性并用时序逻辑公式进行描述,用以支持对安全关键软件的模型检验。最后,以某机载控制系统软件数据处理故障模块的模型检验为例,来说明该方法的有效性和可行性。     

软件安全性研究综述

软件是安全性关键的软件密集型系统(比如综合航电系统)的一个重要安全因子,软件安全性已逐渐成为软件工程和安全工程交又领域的研究热点之一。对软件安全性的内涵与外延进行了剖析,给出了软件安全性定义。讨论了软件安全性的度量模型。着重从软件工程的视角对软件安全性的开发过程、设计方案、评估方法与认证技术等现状进行了综述,并探讨了软件安全性的研究方向。     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

嵌入式自适应安全关键中间件设计方法研究

由于嵌入式安全关键系统自身的特点和应用环境的特殊性,导致了设计嵌入式安全关键应用比一般的嵌入式实时应用要困难得多。在分析传统嵌入式实时中间件技术应用于嵌入式安全关键系统不足的基础上,提出了一种新的自适应安全关键中间件(ASCM)的设计方法,并对相应的体系结构和关键技术进行了讨论。另外,针对嵌入式安全关键系统运行环境的特殊性,重点讨论了一种端到端的自适应服务质量(QoS)管理机制。     

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

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

Scrum与CMMI在中小型安全关键软件中的应用

敏捷方法Scrum可有效解决中小型软件实施CMMI时遇到的诸多问题,但难以满足安全关键软件的特殊需要。对Scrum与CMMI结合的可行性和中小型安全关键软件的主要特征进行了深入分析,在此基础上提出了一种适用于中小型安全关键软件的Scrum与CMMI的结合方法。     

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

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

软件安全需求获取方法的研究

近年来,软件主动式防御思想在软件安全性保障中的地位越来越高,它是一种积极的保障软件安全性的思想,可有效地构建高可信性软件。安全需求的获取是软件安全性保障中最关键的部分,是主动式防御首要完成的任务并且也是最难完成的部分。针对典型的安全需求获取方法,从它们的研究途径、应用情况等方面进行比较和分析,总结并讨论了安全需求获取方法的状况及其未来的发展趋势。上述工作将对安全需求获取方法的研究和实践应用提供有益参考。     

Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System

Reliability of medical devices such as the CARA Infusion Pump Control System is of extreme importance given that these devices are being used on patients in critical condition. The Infusion Pump Control System includes embedded processors and accompanying embedded software for monitoring as well as controlling sensors and actuators that allow the embedded systems to interact with their environments. This nature of the Infusion Pump Control System adds to the complexity of assuring the reliability of the total system. The traditional methods of developing embedded systems are inadequate for such safety-critical devices. In this paper, we study the application of formal methods to the requirements capture and analysis of the Infusion Pump Control System. Our approach consists of two phases. The first phase is to convert the informal design requirements into a set of reference specifications using a formal system, in this case EFSMs (Extended Finite State Machines). The second phase is to translate the reference specifications to the tools supporting formal analysis, such as SCR and Hermes. This allows us to conclude properties of the reference specifications. Our research goal is to develop a framework and methodology for the integrated use of formal methods in the development of embedded medical systems that require high assurance and confidence .     

Integration of informal and formal development of object-oriented safety-critical software

The KeY system allows for the integrated informal and formal development of object-oriented Java software. In this paper we report on a major industrial case study involving safety-critical software for the computation of a particular kind of railway timetable used by train conductors. Our case study includes formal specification of requirements both on the analysis and the implementation level. Particular emphasis in our research is placed on the challenge to make authoring and maintenance of formal specifications easier. We demonstrate that the technique of specification patterns as implemented in KeY for the language OCL yields significant improvements.     

Experimental evaluation of software development tools for safety-critical real-time systems

Since the early years of computing, programmers, systems analysts, and software engineers have sought ways to improve development process efficiency. Software development tools are programs that help developers create other programs and automate mundane operations while bringing the level of abstraction closer to the application engineer. In practice, software development tools have been in wide use among safety-critical system developers. Typical application areas include space, aviation, automotive, nuclear, railroad, medical, and military. While their use is widespread in safety-critical systems, the tools do not always assure the safe behavior of their respective products. This study examines the assumptions, practices, and criteria for assessing software development tools for building safety-critical real-time systems. Experiments were designed for an avionics testbed and conducted on six industry-strength tools to assess their functionality, usability, efficiency, and traceability. The results some light on possible improvements in the tool evaluation process that can lead to potential tool qualification for safety-critical real-time systems.     

一种面向形式化表格需求模型的测试用例生成方法

现代安全关键性系统的软件规模和复杂性的快速增长给这类安全关键性软件系统的开发带来了很多挑战。传统文本文档的需求描述方法无法保证此类系统的开发进度和系统可靠性要求。为此文中提出了一种兼具可读性和可自动分析的形式化表格需求建模方法。文中介绍了一种针对这种表格模型测试用例的自动生成方法,工作包括对该形式化需求表格模型展开语义分析,建立需求模型的控制树结构,得到其测试等价类;为了减少不必要的测试,定义了不同安全级别的软件需求模型的测试覆盖标准,并针对不同覆盖率准则分别给出基于控制树结构的测试路径约束选择方法;对于每条路径约束测试等价类,提出了基于域错误的测试用例选择方法,能够自动生成所需的检测域错误的测试用例集。最后,通过一个需求模型实例展示了所提方法的有效性。     

核安全关键软件的验证与确认技术

介绍了加拿大重水铀反应堆CANDU的安全关键软件的验证与确认(V&V)技术,说明了CANDU核反应堆停堆系统的脱扣计算机及其设计方法,详细描述了用于停堆脱扣计算机软件的确认和可靠性V&R测试的多功能测试平台,以及该测试平台在停堆脱扣计算机软件V&R测试中的应用.V&V技术已被成功地应用于各国CANDU核反应堆停堆系统的脱扣计算机设计中,如韩国的月城CANDU核反应堆、中国的秦山CANDU核反应堆、罗马尼亚Cernavda的2号CANDU核反应堆和加拿大Point Lepreau重建的CANDU核反应堆.随着计算机软硬件技术的发展,所描述的过程和工具在近期的项目中已得到了不断的改善.     

软件安全性3M评价模型复杂度因子的研究

安全苛求系统需要防范意外事件造成对人的生命、大宗财产或环境的损害。因此,对安全苛求软件的测试、安全性评价非常重要。多元、多模型、多阶段的3M评价法能够利用后续测试得到的信息不断对评价因子进行修正,提高了评价的准确性。该文对软件致险缺陷估计模型作了某些改进,然后着重对复杂度因子作了一些研究。     

形式化与可视化相结合的软件体系结构描述方法研究

软件体系结构是软件工程领域中一个重要的研究内容,研究软件体系结构的首要问题是如何描述一个软件系统的体系结构模型。本文通过集成XYZ/ADL与UML两种描述方法在软件体系结构中的应用,寻求一种基于时序逻辑理论的形式化方法与面向对象的可视化方法相结合的软件体系结构描述新途径。着重研究XYZ/ADL与UML在电梯控制系统体系结构建模中的应用问题,并运用基于构件的求精方法对该系统的主要组件进行了求精。