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

ON DETAILED-LEVEL SFMEA METHOD SUPPORTING SPIN VERIFICATION

作　　者：刘畅[1] 李海峰[1] 沈国华[2] 顾益[2] 刘银陵 

机构地区：[1]中国航空综合技术研究所,北京100028 [2]南京航空航天大学,江苏南京200016

出　　处：《计算机应用与软件》2016年第5期281-284,306,共5页Computer Applications and Software

基　　金：国家自然科学基金项目(61272083)

摘　　要：随着软件系统的规模和复杂度不断增大,以软件为核心的安全关键系统的可靠性和安全性越来越难以保证。软件失效模式与影响分析SFMEA(Software Failure Modes and Effect Analysis)是军工业中常用的一种安全分析方法,其依赖人工分析、缺乏形式化语义、无法支持验证。针对SFMEA方法的不足,提出一种结合SPIN的详细级SFMEA方法,对软件失效模式进行形式化建模与分析,并结合模型检验工具SPIN进行自动化地模型检验和模拟仿真,从而提高软件系统的安全性和可靠性。该方法验证了"缓冲区数组下标越界"的这一失效模式,从而说明该方法的有效性。With the increment in scale and complexity of software systems,the reliability and safety of the safety-critical system which taks software as the core are becoming increasingly difficult to guarantee. Software failure mode and effect analysis（ SFMEA） is a common safety analysis method in military industries. However,it depends on manual analysis,lacks the formal semantics and does not support verification.In light of the deficiencies of SFMEA,we propose a detailed-level SFMEA method which combines SPIN to carry out formalised modelling and analysis on software failure mode. Moreover,in combination with model verification tool SPIN it makes automatic model verification and simulation so as to improve the security and reliability of software system. The method validates the failure mode of ＂out of bound of array subscripts in buffer zone＂,therefore explains the effectiveness of the method.

关 键 词：软件FMEA 失效模式 SPIN 安全关键系统 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]