基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法研究.pdf

1、傳統(tǒng)的安全性分析方法，受到分析人員自身技能和經(jīng)驗(yàn)等因素的影響，一定程度上存在容易疏漏系統(tǒng)失效狀態(tài)或誤判失效影響的局限性，因此有必要在飛機(jī)系統(tǒng)安全分析領(lǐng)域中引入新方法。模型檢驗(yàn)方法使用了計(jì)算機(jī)技術(shù)，通過(guò)驗(yàn)證工具列出模型系統(tǒng)的所有狀態(tài)，并能按照邏輯表達(dá)式的描述對(duì)全部狀態(tài)進(jìn)行搜索，在得到安全性分析結(jié)果的同時(shí)能夠降低對(duì)分析人員能力的要求。
　　本文研究了模型檢驗(yàn)理論、計(jì)算機(jī)實(shí)現(xiàn)原理和驗(yàn)證工具，分析總結(jié)了目前通用的飛機(jī)系統(tǒng)安全性評(píng)估流程和安

2、全性分析方法，剖析了故障樹(shù)分析方法流程，指出了其存在的局限性。為此，本文將模型檢驗(yàn)方法應(yīng)用到飛機(jī)系統(tǒng)安全性分析中。以系統(tǒng)需求規(guī)范為分析起點(diǎn)，給出了一種基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析流程。
　　根據(jù)前述工作，本文開(kāi)發(fā)了基于NuSMV安全驗(yàn)證平臺(tái)，平臺(tái)使用了數(shù)據(jù)庫(kù)技術(shù)，建立了基本的元件代碼庫(kù)和失效代碼庫(kù)，可以幫助用戶快速構(gòu)建系統(tǒng)模型、生成驗(yàn)證代碼和知識(shí)庫(kù)文件。最后以ARP4761附錄中的機(jī)輪剎車(chē)系統(tǒng)為例，使用模型檢驗(yàn)方法對(duì)其安全性進(jìn)