一種安全關(guān)鍵軟件驗證方法、裝置、設(shè)備及介質(zhì)

基本信息

申請?zhí)?/td> CN202210031298.7 申請日 -
公開（公告）號 CN114385501A 公開（公告）日 2022-04-22
申請公布號 CN114385501A 申請公布日 2022-04-22
分類號 G06F11/36（2006.01）I;G06F8/10（2018.01）I 分類 計算；推算；計數(shù);
發(fā)明人 吳康;朱守園;牟明;于沛;趙文 申請（專利權(quán)）人 中航機(jī)載系統(tǒng)共性技術(shù)有限公司
代理機(jī)構(gòu) 南京源點知識產(chǎn)權(quán)代理有限公司 代理人 黃啟兵
地址 225000江蘇省揚(yáng)州市廣陵區(qū)廣陵新城江蘇信息服務(wù)產(chǎn)業(yè)基地內(nèi)28號樓B棟11層
法律狀態(tài) -

摘要

摘要 本發(fā)明屬于軟件測試驗證技術(shù)領(lǐng)域，提供了一種安全關(guān)鍵軟件驗證方法、裝置、設(shè)備及介質(zhì)。其中，方法包括：基于LTL語言擴(kuò)展FTA模型得到形式化的系統(tǒng)安全性約束條件及對應(yīng)的軟件需求規(guī)范；將軟件需求規(guī)范按照預(yù)制定轉(zhuǎn)換規(guī)則和MBD的軟件規(guī)范符號匹配，使軟件需求規(guī)范轉(zhuǎn)化為安全規(guī)約模型；將安全規(guī)約模型和預(yù)生成的SCADE軟件設(shè)計模型輸入模型驗證器，完成對軟件的安全性驗證。采用本申請實施例的技術(shù)方案，通過LTL語言進(jìn)行擴(kuò)展使安全性約束條件和安全性約束條件對應(yīng)的軟件需求規(guī)范滿足形式化特征，同時依據(jù)預(yù)制定的轉(zhuǎn)換規(guī)則使軟件需求規(guī)范可以轉(zhuǎn)化為安全規(guī)約模型，用以輸入模型驗證器中進(jìn)行驗證，避免了安全性驗證方法的人為因素的干擾，提高了可靠性。