[發明專利]一種面向航天嵌入式系統的軟件架構開發系統

有效

• 申請號: 202011255814.1
• 申請日: 2020-11-11
• 公開（公告）號: CN112416337B
• 公開（公告）日: 2023-05-02
• 發明（設計）人: 張玉;張晛;王穎;丁敏;劉軍;高飛
• 申請（專利權）人: 北京京航計算通訊研究所
• 主分類號: G06F8/36
• 分類號: G06F8/36;G06F8/35;G06F11/36
• 代理公司: 北京天達知識產權代理事務所有限公司 11386
• 代理人: 李明里

本發明涉及一種面向航天嵌入式系統的軟件架構開發系統，包括：信息提取模塊，用于提取和分類航天型號軟件需求文檔中的軟件關鍵信息；建模驗證模塊，用于對軟件關鍵信息進行形式化建模、驗證與封裝，得到軟件的可復用組件；軟件組件庫，用于存儲所述可復用組件；框架生成模塊，用于構建軟件代碼框架，所述代碼框架由從軟件組件庫中調用的可復用組件構成；軟件代碼編輯模塊，用于在所述軟件代碼框架下，根據軟件的業務邏輯、控制邏輯和算法邏輯編輯軟件代碼，生成可執行軟件本發明可以豐富軟件開發自動化技術、提高軟件開發效率、縮短協議開發周期，提高代碼的安全性和健壯性。

技術領域

本發明屬于軟件工程技術領域，具體涉及一種面向航天嵌入式系統的軟件架構開發系統，其應用于航天嵌入式軟件開發過程中。

背景技術

隨著航天應用的高速發展，其復雜任務需求要求航天嵌入式軟件的算法和處理趨于高度集成化、智能化，軟件規模及復雜度進一步提升，對軟件架構的統一性和軟件的可靠性提出了更高的要求。目前，航天嵌入式軟件研發主要采用任務定制開發模式，由于使用不同的軟件架構，使型號軟件間的繼承性較弱，影響軟件的開發效率和軟件產品的質量。

對于軟件開發架構問題，即使繼承了以往型號的軟件架構，軟件架構中共性資源模塊接口實現不一致、時序不協調等可靠性及安全性設計問題，會影響軟件的可靠性和軟件產品的質量，并且該類問題僅僅依靠單純的軟件開發和軟件測試工作是很難被發現的。

發明內容

鑒于上述的分析，本發明旨在公開了一種面向航天嵌入式系統的軟件架構開發系統，解決航天嵌入式軟件工程領域缺乏通用的嵌入式系統軟件架構，以及提高軟件架構可靠性的問題。

本發明公開了一種面向航天嵌入式系統的軟件架構開發系統，包括：

信息提取模塊，用于提取和分類航天型號軟件需求文檔中的軟件關鍵信息；

建模驗證模塊，用于對軟件關鍵信息進行形式化建模、驗證與封裝，得到軟件的可復用組件；

軟件組件庫，用于存儲所述可復用組件；

框架生成模塊，用于構建軟件代碼框架，所述代碼框架由從軟件組件庫中調用的可復用組件構成；

軟件代碼編輯模塊，用于在所述軟件代碼框架下，根據軟件的業務邏輯、控制邏輯和算法邏輯編輯軟件代碼，生成可執行軟件。

進一步地，還包括軟件缺陷發現模塊，用于根據專家知識庫對生成的所述可執行軟件進行缺陷檢測，定位缺陷位置生成缺陷報告，以輔助可執行軟件的缺陷修復。

進一步地，還包括自主診斷模塊，用于在線監測可執行軟件的運行過程，進行自主診斷、故障定位和故障修復。

進一步地，所述建模驗證模塊包括驗證準則子模塊、建模子模塊、驗證器和封裝子模塊；

所述驗證準則子模塊，用于根據軟件關鍵信息建立軟件形式化驗證準則；

建模子模塊，用于生成軟件的可復用組件，所述可復用組件從軟件架構出發實現多層次復用；

驗證器，用于依據建立的軟件形式化驗證準則對可復用組件進行形式化驗證；

封裝子模塊，用于將通過驗證的可復用組件進行封裝；

具體的，驗證器判斷形式化驗證準則與可復用組件的狀態轉換、時鐘約束是否相符，若相符則通過，將可復用組件輸出到封裝子模塊進行封裝；若狀態轉換不匹配或/和時鐘約束不相符，則將可復用組件返回建模子模塊進行狀態參數修改或/和時間參數修改后，返回驗證器進行重新驗證。

進一步地，所述驗證器的構建過程包括：

建立可更改屬性表格；根據可復用組件實現的功能特點、接口狀態、通訊過程，針對每個組件以表格形式抽象可復用組件的可更改屬性；