隨著安全關(guān)鍵性系統(tǒng)的日益復(fù)雜,如何提高安全關(guān)鍵系統(tǒng)的安全性成為急需解決的問題.基于形式化模型的復(fù)雜系統(tǒng)設(shè)計(jì)與分析是一種重要的安全性分析方法.本文工作對(duì)AIR6110標(biāo)準(zhǔn)中的機(jī)輪剎車實(shí)例系統(tǒng)進(jìn)行了基于形式化方法的安全性分析研究,包括:在系統(tǒng)模型設(shè)計(jì)層級(jí)對(duì)機(jī)輪剎車系統(tǒng)（WBS）的架構(gòu)進(jìn)行層次化分析,將自然語言描述的WBS系統(tǒng)功能用形式化語言（AADL的子集SLIM）進(jìn)行嚴(yán)格的建模描述,消除AIR6110標(biāo)準(zhǔn)中自然語言描述存在的需求語義的二義性,從而建立了WBS系統(tǒng)的形式化模型;考慮系統(tǒng)可能發(fā)生的故障并設(shè)計(jì)多種類的故障模式,基于這些故障模式對(duì)建立的形式化功能模型進(jìn)行失效行為語義的擴(kuò)展,然后對(duì)獲得的擴(kuò)展系統(tǒng)模型進(jìn)行安全性分析.實(shí)例分析論證了基于模型的安全性分析方法在工業(yè)系統(tǒng)中的有效性和實(shí)用性. 

【文章來源】：小型微型計(jì)算機(jī)系統(tǒng). 2020,41(02)北大核心CSCD

【文章頁數(shù)】：6 頁

【部分圖文】：

模型檢查得到錯(cuò)誤屬性的反例

第1個(gè)轉(zhuǎn)換說明，如果收到的數(shù)據(jù)端口綠色液壓值大于等于5，則說明使用正常線路，那么令液壓值等于輸入的綠色液壓值．第2、3、4這三個(gè)轉(zhuǎn)換說明如果收到的綠色液壓值green＿input小于5，則選擇備用線路;收到switch事件，則系統(tǒng)從select＿green轉(zhuǎn)變?yōu)閟elect＿blue，即選擇備用線路;當(dāng)選擇閥收到來自BSCU的select＿alterate值為true，即表示當(dāng)前正常線路出現(xiàn)了問題，則使用備用線路，令選擇閥的輸出液壓值為藍(lán)色液壓值．

它表示電源組件發(fā)生了deplted故障．圖6是導(dǎo)致頂層事件“bscu fail twice”發(fā)生的故障樹．如圖所示，在這個(gè)故障樹中有兩個(gè)分支引起故障:一個(gè)分支是E2和E5，它們通過與門連接，一起導(dǎo)致事件fault＿cfg＿1的發(fā)生;另一個(gè)分支是E2和E6，也通過與門連接，導(dǎo)致事件fault＿cfg＿2的發(fā)生．該故障樹的邏輯公式表示為:(E2∧E5)∨(E2∧E6).

【參考文獻(xiàn)】：
期刊論文
[1]基于SAT求解器的故障樹最小割集求解算法[J]. 羅煒麟,魏歐,黃鳴宇.  計(jì)算機(jī)工程與科學(xué). 2017(04)



本文編號(hào)：3273049