|
|||||
|
|
| 支持SPIN验证的详细级SFMEA方法研究 | |
| 作者单位： | ;1.中国航空综合技术研究所;2.南京航空航天大学 |
| 摘 要： | 随着软件系统的规模和复杂度不断增大,以软件为核心的安全关键系统的可靠性和安全性越来越难以保证。软件失效模式与影响分析SFMEA(Software Failure Modes and Effect Analysis)是军工业中常用的一种安全分析方法,其依赖人工分析、缺乏形式化语义、无法支持验证。针对SFMEA方法的不足,提出一种结合SPIN的详细级SFMEA方法,对软件失效模式进行形式化建模与分析,并结合模型检验工具SPIN进行自动化地模型检验和模拟仿真,从而提高软件系统的安全性和可靠性。该方法验证了"缓冲区数组下标越界"的这一失效模式,从而说明该方法的有效性。 |
| 关 键 词： | 软件FMEA 失效模式 SPIN 安全关键系统 |
ON DETAILED-LEVEL SFMEA METHOD SUPPORTING SPIN VERIFICATION |
|
| Abstract: | |
| Keywords: | |