基于形式化模型检验的飞机系统演绎式安全分析方法研究

发布时间：2024-05-17 17:04

　　传统的演绎式安全性分析由安全性工程师通过手动实施，采用的分析方法主要有故障树分析等，但是这些分析方法都存在一些弊端：高度主观并且依赖分析人员的技能和经验，而且不太可能做到完整无错。如果能将这些时间和精力用于建立所研究系统的模型并对故障模型进行分析，或许能减少通过手动实施所需的耗费并且提高分析的质量。形式化验证技术，如模型检验方法，能够很好地处理复杂度较高的系统，并且能在一定程度上克服这些弊端。 本文分析总结了目前通用的飞机系统安全评估流程及常用的演绎式安全性分析方法，并以故障树分析、可靠性框图等方法为例介绍了分析流程，指出了演绎式安全性分析方法中存在的局限性。为此，通过对形式化模型检验方法的研究，将其引入飞机系统安全分析领域，提出了基于形式化模型检验的飞机系统演绎式安全分析方法，并给出了具体的分析流程。针对模型检验工具输出的可达状态结果集开发了后处理分析平台，对可达状态集进行后续处理分析处理。最后以飞机第二动力系统为案例研究对象，实施了基于形式化模型检验的演绎式安全性分析，得到故障树、最小割集等定性分析结果。

【文章页数】：70 页

【学位级别】：硕士

【部分图文】：

图3.1模型检验过程

图3.1模型检验过程模建模是将待验证的系统用可以被模型检验工具理解的形式化语言进行描单的编程，还需要在对系统及其功能有一定的认识基础上，运用抽象的

图3.5函数f(x1,x2,x3,x4)的ROBDDROBDD具有规范性，即任一布尔函数关于任意的变量排序，都存在唯一的一个ROBDD

如图3.5所示。1x2x3x4x图3.5函数f(x1,x2,x3,x4)的ROBDDROBDD具有规范性，即任一布尔函数关于任意的变量排序，都存在唯一的一个ROBDD。另外，ROBDD的运算时间复杂度也不高，所以其在形式化模型检验中使用非常广泛。3.2.5.2符....

图4.1应用形式化模型检验对飞机系统进行演绎式安全分析

图4.1所示：

图4.2某飞机燃油箱油量监控系统

图4.2某飞机燃油箱油量监控系统系统正常模型一般情况下，待分析的飞机系统的结构及功能都异常复杂，如果对每个零部件细节的话工作量及分析规模都会变得非常庞大，所以在保证系统功能及主要结构不变的前

本文编号：3975866