[發(fā)明專(zhuān)利]一種面向航天嵌入式系統(tǒng)的軟件架構(gòu)設(shè)計(jì)方法

有效

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

1.一種面向航天嵌入式系統(tǒng)的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，包括如下步驟：

生成嵌入式軟件組件庫(kù)，所述嵌入式軟件組件庫(kù)包括經(jīng)過(guò)形式化驗(yàn)證的可復(fù)用組件；

從所述嵌入式軟件組件庫(kù)中選擇所需的可復(fù)用組件，構(gòu)建嵌入式軟件代碼框架；

根據(jù)所述嵌入式軟件代碼框架，進(jìn)行嵌入式軟件代碼編輯，生成可執(zhí)行軟件；

根據(jù)專(zhuān)家知識(shí)庫(kù)對(duì)生成的所述可執(zhí)行軟件進(jìn)行缺陷檢測(cè)，定位缺陷位置生成缺陷報(bào)告，并進(jìn)行缺陷修復(fù)；

在線監(jiān)測(cè)可執(zhí)行軟件的運(yùn)行過(guò)程，進(jìn)行自主診斷、故障定位和故障修復(fù)；

所述形式化驗(yàn)證包括以下步驟：

1）構(gòu)建用于組件屬性抽象、修改和形式化驗(yàn)證的驗(yàn)證器；

2）使用驗(yàn)證器對(duì)可復(fù)用組件進(jìn)行驗(yàn)證；

3）判斷驗(yàn)證是否通過(guò)；通過(guò)，則將可復(fù)用組件存入軟件組件庫(kù)；不通過(guò)，則修訂可復(fù)用組件的參數(shù)，返回步驟2）進(jìn)行重新驗(yàn)證；

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

建立可更改屬性表格；根據(jù)可復(fù)用組件實(shí)現(xiàn)的功能特點(diǎn)、接口狀態(tài)、通訊過(guò)程，針對(duì)每個(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)系；通過(guò)字段匹配，將可更改屬性表格與可復(fù)用組件XML文件進(jìn)行關(guān)聯(lián)；用戶(hù)通過(guò)修改組件屬性表格實(shí)現(xiàn)對(duì)可復(fù)用組件XML文件的自動(dòng)修改；

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

2.根據(jù)權(quán)利要求1所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，所述生成嵌入式軟件組件庫(kù)，包括：

1）提取航天型號(hào)軟件需求中的軟件關(guān)鍵信息，分類(lèi)建立軟件形式化驗(yàn)證準(zhǔn)則；

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

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

4）將通過(guò)驗(yàn)證的組件進(jìn)行封裝，得到所述嵌入式軟件組件庫(kù)。

3.根據(jù)權(quán)利要求2所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，所述軟件形式化驗(yàn)證準(zhǔn)則包括接口驗(yàn)證準(zhǔn)則、時(shí)序驗(yàn)證準(zhǔn)則和交互關(guān)系驗(yàn)證準(zhǔn)則。

4.根據(jù)權(quán)利要求3所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，所述接口驗(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)則。

5.根據(jù)權(quán)利要求1所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，可復(fù)用組件的可復(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ù)查詢(xún)服務(wù)、事件服務(wù)和總線服務(wù)；數(shù)據(jù)管理層，用于封裝不同的數(shù)據(jù)處理功能模塊，包括實(shí)現(xiàn)具體功能的函數(shù)，提供可調(diào)用的API給主控層；所述主控層，用于通過(guò)調(diào)用API實(shí)現(xiàn)對(duì)業(yè)務(wù)處理流程的控制。

6.根據(jù)權(quán)利要求1所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，

所述缺陷檢測(cè)過(guò)程包括：

對(duì)軟件代碼進(jìn)行詞義分析、語(yǔ)義分析，提取并計(jì)算時(shí)序特征；

識(shí)別軟件所表達(dá)的功能語(yǔ)義，確保正確、合理的功能語(yǔ)義；

對(duì)于發(fā)現(xiàn)的軟件缺陷利用各種信息，判斷問(wèn)題發(fā)生的原因，定位缺陷發(fā)生的程序單元或語(yǔ)句，生成缺陷報(bào)告。

7.根據(jù)權(quán)利要求1所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，

所述專(zhuān)家知識(shí)庫(kù)包括軟件設(shè)計(jì)知識(shí)以及待求解問(wèn)題相關(guān)的軟件測(cè)試和軟件實(shí)驗(yàn)的相關(guān)知識(shí)。

8.根據(jù)權(quán)利要求1所述的軟件架構(gòu)設(shè)計(jì)方法，其特征在于，

所述在線監(jiān)測(cè)可執(zhí)行軟件運(yùn)行過(guò)程，對(duì)軟件運(yùn)行中的SEU故障進(jìn)行自主診斷，發(fā)現(xiàn)軟件運(yùn)行中的故障，進(jìn)行故障檢測(cè)、故障定位、故障修復(fù)。