[發(fā)明專利]基于模型轉(zhuǎn)換的民用飛機(jī)系統(tǒng)行為狀態(tài)安全性驗(yàn)證方法

在審

• 申請?zhí)枺?/td>: 202110570192.X
• 申請日: 2021-05-25
• 公開（公告）號: CN113283008A
• 公開（公告）日: 2021-08-20
• 發(fā)明（設(shè)計(jì)）人: 榮灝;張福凱;李娜;周元輝;張茂帝;林謝貴;陳龍;楊亮;姜軼;周海燕;谷青范
• 申請（專利權(quán)）人: 中國航空無線電電子研究所
• 主分類號: G06F30/15
• 分類號: G06F30/15;G06F30/20
• 代理公司: 上海和躍知識產(chǎn)權(quán)代理事務(wù)所(普通合伙) 31239
• 代理人: 楊慧

1.一種基于模型轉(zhuǎn)換的民用飛機(jī)系統(tǒng)行為狀態(tài)安全性驗(yàn)證方法，其特征在于包含以下步驟：

步驟1、根據(jù)民用飛機(jī)系統(tǒng)中各組件之間的功能交互關(guān)系構(gòu)建AltaRica GTS模型；

步驟2、以驗(yàn)證民用飛機(jī)系統(tǒng)的行為狀態(tài)為目標(biāo)，確定GTS模型與NuSMV模型之間的映射規(guī)則，將GTS模型轉(zhuǎn)換為NuSMV模型；

步驟3、利用NuSMV工具對轉(zhuǎn)換后的NuSMV模型開展系統(tǒng)行為狀態(tài)的安全性驗(yàn)證。

2.根據(jù)權(quán)利要求1所述的一種基于模型轉(zhuǎn)換的民用飛機(jī)系統(tǒng)行為狀態(tài)安全性驗(yàn)證方法，其特征在于所述步驟1包含以下步驟：

步驟1-1，從系統(tǒng)架構(gòu)交聯(lián)關(guān)系的角度，梳理待進(jìn)行驗(yàn)證的民用飛機(jī)系統(tǒng)中的各組件之間的功能交互關(guān)系，功能交互關(guān)系包括各組件的名稱、輸入接口、輸出接口和故障模式；

步驟1-2、根據(jù)AltaRica GTS模型定義規(guī)則，將梳理的功能交互關(guān)系轉(zhuǎn)換為AltaRicaGTS模型；AltaRica GTS模型定義規(guī)則為：node下定義的組件名稱，flow下定義的組件的輸入接口、輸出接口，assert下定義組件的故障邏輯表達(dá)式。

3.根據(jù)權(quán)利要求2所述的一種基于模型轉(zhuǎn)換的民用飛機(jī)系統(tǒng)行為狀態(tài)安全性驗(yàn)證方法，其特征在于所述步驟2包含以下步驟：

步驟2-1：GTS模型向NuSMV正常模塊轉(zhuǎn)換：首先將AltaRica GTS模型中的各組件的名稱和flow中定義的輸入接口轉(zhuǎn)換為NuSMV正常模塊的定義信息；然后，通過固定的正常和故障的兩種值定義status狀態(tài)，并將AltaRica GTS模型中的flow中定義的輸出接口轉(zhuǎn)換為NuSMV正常模塊的狀態(tài)變量所屬的組件輸出名稱；最后，在NuSMV中定義轉(zhuǎn)移關(guān)系和條件時(shí)，默認(rèn)組件初始狀態(tài)為正常值nominal，接下來根據(jù)AltaRica GTS模型中的assert定義的故障邏輯表達(dá)式轉(zhuǎn)換過NuSMV正常模塊的組件輸出與組件狀態(tài)及其輸入之間的致因關(guān)系；

步驟2-2：GTS模型向NuSMV故障模塊轉(zhuǎn)換：首先將AltaRica GTS模型中的各組件的名稱和flow中定義的輸入接口轉(zhuǎn)換為NuSMV故障模塊的故障模塊定義信息；然后，將AltaRicaGTS模型中的各組件的名稱和flow中定義的輸出接口轉(zhuǎn)換為故障模塊的聲明，定義組件故障時(shí)的狀態(tài)變量取值。

4.根據(jù)權(quán)利要求1所述的一種基于模型轉(zhuǎn)換的民用飛機(jī)系統(tǒng)行為狀態(tài)安全性驗(yàn)證方法，其特征在于所述步驟3包含以下步驟：

步驟3-1：將轉(zhuǎn)換后的NuSMV模型導(dǎo)入NuSMV工具中，確定系統(tǒng)的安全屬性規(guī)約，定義計(jì)算樹邏輯；

步驟3-2：利用NuSMV工具開展模型檢查，自動(dòng)地驗(yàn)證所轉(zhuǎn)換后的系統(tǒng)模型是否滿足系統(tǒng)的安全屬性規(guī)約；如果不滿足則會(huì)給出反例執(zhí)行序列，示意其中未覆蓋的系統(tǒng)行為狀態(tài)；通過分析反例序列中變化的狀態(tài)量，確定導(dǎo)致不期望事件發(fā)生的狀態(tài)或狀態(tài)組合，針對不期望事件開展安全性設(shè)計(jì)。