傳統(tǒng)的演繹式安全性分析由安全性工程師通過手動實施，采用的分析方法主要有故障樹分析等，但是這些分析方法都存在一些弊端：高度主觀并且依賴分析人員的技能和經驗，而且不太可能做到完整無錯。如果能將這些時間和精力用于建立所研究系統(tǒng)的模型并對故障模型進行分析，或許能減少通過手動實施所需的耗費并且提高分析的質量。形式化驗證技術，如模型檢驗方法，能夠很好地處理復雜度較高的系統(tǒng)，并且能在一定程度上克服這些弊端。 本文分析總結了目前通用的飛機系統(tǒng)安全評估流程及常用的演繹式安全性分析方法，并以故障樹分析、可靠性框圖等方法為例介紹了分析流程，指出了演繹式安全性分析方法中存在的局限性。為此，通過對形式化模型檢驗方法的研究，將其引入飛機系統(tǒng)安全分析領域，提出了基于形式化模型檢驗的飛機系統(tǒng)演繹式安全分析方法，并給出了具體的分析流程。針對模型檢驗工具輸出的可達狀態(tài)結果集開發(fā)了后處理分析平臺，對可達狀態(tài)集進行后續(xù)處理分析處理。最后以飛機第二動力系統(tǒng)為案例研究對象，實施了基于形式化模型檢驗的演繹式安全性分析，得到故障樹、最小割集等定性分析結果。

【文章頁數】：70 頁

【學位級別】：碩士

【部分圖文】：

圖3.1模型檢驗過程

圖3.1模型檢驗過程模建模是將待驗證的系統(tǒng)用可以被模型檢驗工具理解的形式化語言進行描單的編程，還需要在對系統(tǒng)及其功能有一定的認識基礎上，運用抽象的

圖3.5函數f(x1,x2,x3,x4)的ROBDDROBDD具有規(guī)范性，即任一布爾函數關于任意的變量排序，都存在唯一的一個ROBDD

如圖3.5所示。1x2x3x4x圖3.5函數f(x1,x2,x3,x4)的ROBDDROBDD具有規(guī)范性，即任一布爾函數關于任意的變量排序，都存在唯一的一個ROBDD。另外，ROBDD的運算時間復雜度也不高，所以其在形式化模型檢驗中使用非常廣泛。3.2.5.2符....

圖4.1應用形式化模型檢驗對飛機系統(tǒng)進行演繹式安全分析

圖4.1所示：

圖4.2某飛機燃油箱油量監(jiān)控系統(tǒng)

圖4.2某飛機燃油箱油量監(jiān)控系統(tǒng)系統(tǒng)正常模型一般情況下，待分析的飛機系統(tǒng)的結構及功能都異常復雜，如果對每個零部件細節(jié)的話工作量及分析規(guī)模都會變得非常龐大，所以在保證系統(tǒng)功能及主要結構不變的前

本文編號：3975866