[發(fā)明專利]一種面向航天嵌入式系統(tǒng)的軟件架構(gòu)開發(fā)系統(tǒng)

有效

• 申請?zhí)枺?/td>: 202011255814.1
• 申請日: 2020-11-11
• 公開（公告）號: CN112416337B
• 公開（公告）日: 2023-05-02
• 發(fā)明（設(shè)計(jì)）人: 張玉;張晛;王穎;丁敏;劉軍;高飛
• 申請（專利權(quán)）人: 北京京航計(jì)算通訊研究所
• 主分類號: G06F8/36
• 分類號: G06F8/36;G06F8/35;G06F11/36
• 代理公司: 北京天達(dá)知識產(chǎn)權(quán)代理事務(wù)所有限公司 11386
• 代理人: 李明里

1.一種面向航天嵌入式系統(tǒng)的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，包括：

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

建模驗(yàn)證模塊，用于對軟件關(guān)鍵信息進(jìn)行形式化建模、驗(yàn)證與封裝，得到軟件的可復(fù)用組件；

軟件組件庫，用于存儲所述可復(fù)用組件；

框架生成模塊，用于構(gòu)建軟件代碼框架，所述代碼框架由從軟件組件庫中調(diào)用的可復(fù)用組件構(gòu)成；

軟件代碼編輯模塊，用于在所述軟件代碼框架下，根據(jù)軟件的業(yè)務(wù)邏輯、控制邏輯和算法邏輯編輯軟件代碼，生成可執(zhí)行軟件；

所述建模驗(yàn)證模塊包括驗(yàn)證準(zhǔn)則子模塊、建模子模塊、驗(yàn)證器和封裝子模塊；

所述驗(yàn)證準(zhǔn)則子模塊，用于根據(jù)軟件關(guān)鍵信息建立軟件形式化驗(yàn)證準(zhǔn)則；

建模子模塊，用于生成軟件的可復(fù)用組件，所述可復(fù)用組件從軟件架構(gòu)出發(fā)實(shí)現(xiàn)多層次復(fù)用；

驗(yàn)證器，用于依據(jù)建立的軟件形式化驗(yàn)證準(zhǔn)則對可復(fù)用組件進(jìn)行形式化驗(yàn)證；

封裝子模塊，用于將通過驗(yàn)證的可復(fù)用組件進(jìn)行封裝；

具體的，驗(yàn)證器判斷形式化驗(yàn)證準(zhǔn)則與可復(fù)用組件的狀態(tài)轉(zhuǎn)換、時(shí)鐘約束是否相符，若相符則通過，將可復(fù)用組件輸出到封裝子模塊進(jìn)行封裝；若狀態(tài)轉(zhuǎn)換不匹配或/和時(shí)鐘約束不相符，則將可復(fù)用組件返回建模子模塊進(jìn)行狀態(tài)參數(shù)修改或/和時(shí)間參數(shù)修改后，返回驗(yàn)證器進(jìn)行重新驗(yàn)證；

所述驗(yàn)證器的構(gòu)建過程包括：

建立可更改屬性表格；根據(jù)可復(fù)用組件實(shí)現(xiàn)的功能特點(diǎn)、接口狀態(tài)、通訊過程，針對每個(gè)組件以表格形式抽象可復(fù)用組件的可更改屬性；

建立可復(fù)用組件XML文件；確定可復(fù)用組件的工作狀態(tài)以及觸發(fā)事件、時(shí)鐘約束、控制流設(shè)置和狀態(tài)轉(zhuǎn)換事件，利用時(shí)間自動(dòng)機(jī)模型的形式化方法進(jìn)行建模，每個(gè)可復(fù)用組件生成一個(gè)可復(fù)用組件XML文件；

建立關(guān)聯(lián)關(guān)系；通過字段匹配，將可更改屬性表格與可復(fù)用組件XML文件進(jìn)行關(guān)聯(lián)；用戶通過修改組件屬性表格實(shí)現(xiàn)對可復(fù)用組件XML文件的自動(dòng)修改；

將可復(fù)用組件XML文件導(dǎo)入U(xiǎn)PPAAL工具，建立一個(gè)用于組件屬性抽象、修改和形式化驗(yàn)證的驗(yàn)證器。

2.根據(jù)權(quán)利要求1所述的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，還包括軟件缺陷發(fā)現(xiàn)模塊，用于根據(jù)專家知識庫對生成的所述可執(zhí)行軟件進(jìn)行缺陷檢測，定位缺陷位置生成缺陷報(bào)告，以輔助可執(zhí)行軟件的缺陷修復(fù)。

3.根據(jù)權(quán)利要求2所述的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，還包括自主診斷模塊，用于在線監(jiān)測可執(zhí)行軟件的運(yùn)行過程，進(jìn)行自主診斷、故障定位和故障修復(fù)。

4.根據(jù)權(quán)利要求1所述的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，所述軟件形式化驗(yàn)證準(zhǔn)則包括接口驗(yàn)證準(zhǔn)則、時(shí)序驗(yàn)證準(zhǔn)則和交互關(guān)系驗(yàn)證準(zhǔn)則。

5.根據(jù)權(quán)利要求4所述的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，所述接口驗(yàn)證準(zhǔn)則包括總線接口、數(shù)據(jù)傳輸接口在內(nèi)的物理接口的驗(yàn)證準(zhǔn)則；

所述時(shí)序驗(yàn)證準(zhǔn)則包括狀態(tài)有界響應(yīng)、多狀態(tài)并發(fā)、時(shí)間約束和先后順序在內(nèi)的驗(yàn)證準(zhǔn)則；

所述交互關(guān)系驗(yàn)證準(zhǔn)則包括應(yīng)答通信、嵌套調(diào)用、多播通信、同步通信在內(nèi)的驗(yàn)證準(zhǔn)則。

6.根據(jù)權(quán)利要求1所述的軟件架構(gòu)開發(fā)系統(tǒng)，其特征在于，可復(fù)用組件包括主控層、數(shù)據(jù)管理層、調(diào)度管理層和接口驅(qū)動(dòng)層；

其中，

所述接口驅(qū)動(dòng)層，用于完成接口的初始配置和加載，提供底層接口服務(wù)，為軟件提供正常運(yùn)行的基礎(chǔ)；

所述調(diào)度管理層，用于實(shí)現(xiàn)接口驅(qū)動(dòng)層和數(shù)據(jù)管理層之間的服務(wù)橋梁，所述服務(wù)包括函數(shù)調(diào)用服務(wù)、中斷處理服務(wù)、任務(wù)查詢服務(wù)、事件服務(wù)和總線服務(wù)；

數(shù)據(jù)管理層，用于封裝不同的數(shù)據(jù)處理功能模塊，包括實(shí)現(xiàn)具體功能的函數(shù)，提供可調(diào)用的API給主控層；

所述主控層，用于通過調(diào)用API實(shí)現(xiàn)對業(yè)務(wù)處理流程的控制。