安全關(guān)鍵系統(tǒng)需求形式化建模分析實例研究
摘要：近年來,基于模型的安全性分析技術(shù)(MBSA)在航空等領(lǐng)域有著廣泛應(yīng)用,因此對以xSAP安全分析平臺為核心,基于MBSA的系統(tǒng)安全性評估方法進行了研究,并通過一個真實的綜合航電系統(tǒng)GarminG1000的自動飛行控制系統(tǒng)(AFCS)GFC700為實例來詳細介紹。該方法的實現(xiàn)包括使用NuSMV形式化語言對系統(tǒng)進行需求建模,根據(jù)系統(tǒng)設(shè)計故障模式,在NuSMV模型中注入故障事件,使用xSAP對NuSMV需求模型進行模型擴展得到故障擴展模型,以及對故障擴展模型進行故障分析及系統(tǒng)安全性評估,例如生成故障樹及FMEA表等。從分析結(jié)果來看,使用xSAP平臺對實際系統(tǒng)進行基于模型的系統(tǒng)安全分析是行之有效的。
注: 保護知識產(chǎn)權(quán),如需閱讀全文請聯(lián)系計算機科學(xué)與探索雜志社
相關(guān)推薦
更多
用研究.jpg)
學(xué)報.jpg)
與探索.jpg)
于我們.jpeg)