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

被引：4

作者：

王飞 ^{[1
]}

沈国华 ^{[1
]}

黄志球 ^{[1
]}

马琳 ^{[1
]}

刘畅 ^{[2
]}

李海峰 ^{[2
]}

廖莉莉 ^{[1
]}

机构：

[1] 南京航空航天大学计算机科学与技术学院

[2] 中国航空综合技术研究所

来源：

计算机科学 | 2015年 / 42卷 / 12期

关键词：

故障树分析; 模型检验; 线性时序逻辑; 安全关键系统; 安全属性;

D O I：

暂无

中图分类号：

TP311.53 [];

学科分类号：

摘要：

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

引用

页码：71 / 75

页数：5

共 8 条

[1]

软件时序故障树建模与分析技术研究 [D].