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

有效

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

技術領域

本發明屬于計算機軟件設計技術領域，涉及一種模型自動化驗證方法，具體涉及一種符合DO-178B/C?A級軟件的模型驗證方法。

背景技術

DO-178B/C《機載系統和設備合格審定中的軟件考慮》是美國航空無線電委員會(The?Radio?Technical?Commission?for?Aeronautics,RTCA)提出的航空適航認證標準，A級是機載軟件開發要求的最高級別。1992年RTCA發布了DO-178B《機載系統和設備合格審定中的軟件考慮》。DO-178C于2012年12月頒布執行。與DO-178B相比，DO-178C在保證標準的主體部分的穩定性的同時用附錄的形式提出了對特定問題或技術方法的目標要求，如工具鑒定、面向對象方法、模型開發方法等、形式化方法等。機載軟件開發符合DO-178B/C標準的要求，是其通過認證機載使用的必要條件。A級軟件的研發按照DO-178B/C的要求，分為軟件計劃、軟件開發與軟件綜合三個過程。在軟件計劃階段，需對軟件生命周期、軟件開發、驗證環境進行策劃。在軟件開發過程中，需執行軟件需求、軟件設計、軟件編碼與軟件集成；在綜合過程中需執行軟件驗證、軟件配置管理、軟件質量保證和軟件合格審定聯絡。DO-178B/C標準只定義了上述過程的目標要求，但并未提及采用何種方法來執行這些過程。

發明內容

為了解決背景技術中的問題，本發明以DO-178B/C中提出的模型開發技術為基礎，提出一種符合DO-178B/C軟件的模型驗證方法能夠通過當前軟件建模工具生成軟件模型，根據軟件級別，生成滿足適航要求的驗證程序集，為機載軟件的適航合格審定提供有力支持。

本發明的具體技術方案是：

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

1)搭建驗證系統架構；

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

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

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

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

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

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

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

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

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

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

上述驗證數據生成器根據數據類型及其約束的定義，生成驗證數據樣本，包括正常輸入和異常輸入數據；建立驗證數據的等價類定義，采用隨機驗證、邊界值分析的方法生成驗證數據集；

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

上述驗證程序生成和選取器包括驗證程序信息定義模塊、驗證環境配置模塊、驗證程序選取模塊；

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

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

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

上述數據類型建模包括數據類型定義模塊和數據類型約束定義模塊；

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