[發明專利]一種符合DO-178B/C A級軟件的模型驗證方法

有效

• 申請號: 201410728455.5
• 申請日: 2014-11-29
• 公開（公告）號: CN104461882A
• 公開（公告）日: 2015-03-25
• 發明（設計）人: 田莉蓉;邢亮;牟明;戴小氐;黃暉;逯計劃
• 申請（專利權）人: 中國航空工業集團公司第六三一研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 西安智邦專利商標代理有限公司 61211
• 代理人: 王少文

1.一種符合DO-178B/C?A級軟件的模型驗證方法，其特征在于，包括以下步驟：

1)搭建驗證系統架構；

所述驗證系統架構包括模型轉換層、驗證數據和邏輯生成層、驗證程序生成和選取層；

所述模型轉換層通過模型轉換器將輸入模型轉換為若干個特征模型；所述模型轉換器的轉換過程為數據類型建模和特征服務建模的過程；

所述驗證數據生成層將若干個特征模塊分別通過驗證數據生成器生成驗證數據集，通過驗證邏輯生成器生成驗證邏輯集；

所述驗證程序生成和選擇層通過驗證程序生成和選擇器將驗證數據集和驗證邏輯集生成為驗證程序集；

2)用戶將待驗證模型輸入至模型轉換層中的，待驗證模型通過模型轉換器轉換為若干個特征模型；

3)以若干個特征模型輸入至驗證數據和邏輯生成層通過驗證數據生成器和驗證邏輯生成器生成驗證數據集和驗證邏輯集；

4)利用驗證程序生成和選擇層中的驗證程序生成和選擇器將驗證數據集和驗證邏輯集生成驗證程序集；從驗證程序集中選取出驗證程序子集；

5)根據驗證程序子集通過DO-178B/C中要求的軟件覆蓋強度級別進行驗證；若驗證成功，則待驗證模型通過驗證；

若驗證失敗，則待驗證模型未通過驗證；

所述覆蓋強度級別包括語句判定、修訂的條件以及判定覆蓋。

2.根據權利要求1所述的符合DO-178B/C?A級軟件的模型驗證方法，其特征在于：所述驗證數據生成器根據數據類型及其約束的定義，生成驗證數據樣本，包括正常輸入和異常輸入數據；建立驗證數據的等價類定義，采用隨機驗證、邊界值分析的方法生成驗證數據集；

所述驗證邏輯生成器根據特征模型，接口之間的約束和依賴關系，采用組合驗證的方式，生成不同組合覆蓋率的驗證數據，確定驗證過程中的驗證邏輯集。

3.根據權利要求1所述的符合DO-178B/C?A級軟件的模型驗證方法，其特征在于：所述驗證程序生成和選取器包括驗證程序信息定義模塊、驗證環境配置模塊、驗證程序選取模塊；

所述驗證程序信息定義模塊的信息輸入源是驗證人員手工配置的驗證用例模版；所述模版使用XML文本，所述模版主要包括驗證項目中驗證用例的共有信息，所述驗證程序信息定義模塊利用用例模版，把驗證驗證數據集與驗證邏輯集進行組裝，生成正常驗證用例和異常驗證用例；根據特征服務模型中的服務前置條件、服務后置條件和服務約束，按照依賴次序和驗證目標，對若干驗證用例進行組合，生成驗證程序集；

所述驗證環境配置模塊用于配置驗證的驗證環境，所述驗證環境包括宿主機型號、目標機型號、操作系統配置、內存配置、各種工具包；

所述驗證程序選取模塊根據所述驗證程序集和驗證環境以及DO-178B中定義的軟件級別選取出不同的驗證程序子集。

4.根據權利要求1所述的符合DO-178B/C?A級軟件的模型驗證方法，其特征在于：所述數據類型建模包括數據類型定義模塊和數據類型約束定義模塊；

所述數據類型定義模塊用于定義簡單類型描述、定義枚舉類型描述以及定義結構體類型描述；

所述數據類型約束定義模塊用于定義有效值枚舉、定義長度約束以及定義區間約束；

所述特征服務建模包括服務基本信息定義模塊和服務參數信息定義模塊；

所述服務基本信息定義模塊用于定義服務描述、定義服務前置條件、定義服務后置條件以及定義服務約束；

所述服務參數信息定義模塊定義服務參數的基本信息、定義服務參數的數據池。