《高可信嵌入式軟體建模與驗證方法的研究》是依託南京航空航天大學，由莊毅擔任項目負責人的面上項目。
基本介紹
- 中文名：高可信嵌入式軟體建模與驗證方法的研究
- 項目類別：面上項目
- 項目負責人：莊毅
- 依託單位：南京航空航天大學
項目摘要,結題摘要,
項目摘要
近年來，軟體的可信性已成為綜合反映軟體質量狀態的新度量。與普通軟體相比，嵌入式軟體由於其特殊的套用領域，還具有實時性、高可靠性、高安全性等高可信性需求。面對日益嚴峻的信息安全和軟體規模不斷增大等問題，在高可信嵌入式軟體的需求分析、設計、實現、測試、以及運維等各階段均面臨新的困難和挑戰。本項目的研究將為解決上述問題提供理論基礎，提出建模與驗證的新方法。.本項目立足於高可信嵌入式軟體的建模與驗證基礎理論和方法的研究。旨在為高可信嵌入式軟體的建模與驗證建立理論框架，建立可信指標體系，並提出建模與驗證新方法。研究工作將半形式化與形式化方法相結合，提出高可信嵌入式軟體建模與驗證理論框架；提出一種可刻畫高可信約束的嵌入式軟體模型Z-MARTE和動態行為模型ZMTA；進一步，提出高可信嵌入式軟體的建模方法和驗證方法，設計相關流程，並對相應的實現技術開展研究；最後，通過航空領域中的機載軟體實例開展套用研究與實驗。
結題摘要
軟體可信性已成為綜合反映軟體質量狀態的新度量。本項目研究了面向高可信嵌入式軟體可信屬性的定義方法，建立了層次化的嵌入式軟體可信屬性指標體系，給出了各子屬性的可信度量項及度量方法，可為嵌入式軟體可信屬性建模與驗證提供依據；項目組擴展了Z語言的元模型，提出了一種可擴展的可信嵌入式軟體模型 Z-MARTE，包括時間模型、結構模型、行為模型、可靠性模型、安全模型等Z-MARTE子模型，該模型能夠在軟體靜態結構與動態行為的雙重視角下，描述包括數據約束與時間約束等各類可信約束，為嵌入式軟體可信屬性的建模提供了一種有效途徑，為軟體的分析、驗證與評估提供了語義基礎；提出了一種基於模型檢測技術的嵌入式軟體可信性驗證方法，提出了有限域Z-MARTE動態模型上的模型檢測算法FZMCA，可用於解決嵌入式軟體行為中可信約束的驗證問題；提出了一種基於Z語言的嵌入式軟體對象-訊息-角色模型OMR，以OMR模型中的軟體對象為評估單位，以對象間的通信行為規範與軟體安全約束為評估依據，提出了一種嵌入式軟體風險評估方法RAMES，從數據流安全的角度對嵌入式軟體的安全性進行風險評估；提出了基於一致性強度的安全關鍵嵌入式軟體的模糊評估方法，能夠處理軟體評估、信息安全風險評估中出現的模糊值和殘缺值問題；提出了一種適用於實時嵌入式軟體安全屬性的形式化模型ZMsec，定義了ZMsec用例模型、靜態模型和動態模型。該模型可描述嵌入式軟體的時間/安全約束，增強了對嵌入式軟體安全特徵的表達能力。定義了時序邏輯公式ZMsecTL用於描述嵌入式軟體安全屬性，提出了ZMsecSD算法，將ZMsec模型轉換為嵌入式軟體安全狀態轉移圖，用於模型檢測和反例生成，可有效驗證嵌入式軟體的安全性。項目組已發表/錄用SCI期刊論文14篇，授權發明專利2項，公開發明專利6項。研究成果獲得了國內外多位學者的好評。本項目的研究成果可為嵌入式可信軟體的研發與評估提供技術基礎，具有很好的科學意義。其研究成果在航空和船舶等可信關鍵領域已進行了套用研究，具有很好的套用前景。
