基于故障树的航电软件系统安全性验证方法研究

摘要

嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为当前的研究热点。故障树能够自底向上地描述软件失效发生的因果关系链，可以通过故障树分析，从中提取出系统安全属性，但是却无法验证系统本身是否满足这些安全属性。而且由于其非形式化方法的局限性，传统的故障树也无法精确描述安全关键系统中具有时序特征的系统故障。计算机领域的模型检验技术能够对待验证系统的相关性质进行精确地验证，并准确定位错误执行轨迹，但在待验证性质的提取方面仍存在着技术瓶颈。
　　本文结合传统故障树分析的系统性与模型检验形式化表达的精确性等优点，提出一种基于故障树分析的软件安全性验证方法。首先，对传统故障树进行扩充，并结合形式化方法提出一种用线性时序逻辑规约的能够描述软件系统时序故障的线性时序故障树——LTFT，并根据安全性验证的需求给出一套支持安全属性验证的LTFT约简规则。然后，利用LTFT的特点改进了传统故障树的割集分析算法，提出一个基于LTFT割集分析的安全属性提取算法，并运用该算法提取出LTFT所描述的软件系统安全属性。再针对安全属性对软件系统抽象建模并对软件模型进行验证，判断该安全属性在软件的设计中是否得到满足，为软件安全性验证提供有效证据。最后，通过对工程实践中的一个飞机襟缝翼控制系统进行故障树建模和安全属性提取，并用本文自行开发的一款基于SPIN的图形化软件模型检验工具——Espin对其进行安全性验证，对验证结果进行分析，最终说明了文章方法的可行性和有效性。

目录

封面

声明

中文摘要

英文摘要

目录

图表清单

注释表

第一章 绪论

1.1 课题研究背景

1.2 国内外研究现状及选题依据

1.3 论文的组织结构

第二章 传统故障树分析法和模型检验

2.1 传统故障树分析法（FTA）

2.2 模型检验

2.3 FTA与模型检验的结合

2.4 本章小结

第三章 线性时序故障树（LTFT）的构建及约简

3.1 用线性时序逻辑形式化规约的LTFT

3.2 LTFT约简

3.3 本章小结

第四章 LTFT安全属性提取及验证

4.1 LTFT安全属性提取

4.2 软件系统形式化建模

4.3 软件模型安全属性验证

4.4 本章小结

第五章 航电软件系统实例研究

5.1 软件系统故障树构建

5.2 软件系统LTFT构建及约简

5.3 软件系统安全属性提取与验证

5.4 本章小结

第六章 总结与展望

6.1 论文总结

6.2 未来工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文

附录 襟缝翼控制系统传统故障树与LTFT―故障事件——形式化命名‖映射表