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