基于模型的方法在民機機載軟件中的應用

作者 | 蔡喁上海控安可信軟件創(chuàng)新研究院副院長

版塊 |鑒源論壇 · 觀擎

社群 |添加微信號“TICPShanghai”加入“上?？匕?1fusa安全社區(qū)”

01基于模型的開發(fā)和驗證MBDV

模型泛指用于支持軟件開發(fā)過程或軟件驗證過程的系統(tǒng)的一組軟件方面的抽象表示，在機載軟件中，基于模型的開發(fā)和驗證中所涉及的模型一般包含以下特征：

1.使用明確標識的建模符號來完全描述模型。這里所說的建模符號可以是圖形和/或文本的。

2.該模型包含軟件需求和/或軟件體系結構定義。

3.該模型的形式和類型用于軟件開發(fā)過程或軟件再驗證過程支持的直接分析或行為評估。

相比之下一些其他類型的“類模型方法”在機載軟件領域內并不被定義為一種MBDV方法。包括無法形成語法語義有限閉環(huán)的圖形表達方法、或者在機載軟件生命周期中無法用于表達需求/設計的圖文結合表達方法。

之所以在民機機載軟件中對模型開發(fā)進行如此的定義，與民用飛機所面臨的適航符合性要求是相關的。正如前面幾期介紹的，機載軟件適航標準對軟件研制過程、生命周期數據以及符合性證據等都提出了明確的要求。然而，這些過程要求都是建立在歐美80~90年代軟件工程實踐的基礎上，以文本需求+代碼為主要的開發(fā)方式。隨著近些年模型技術的進步，很多研制方法中通過模型表達需求或者設計，從而改變了以往單純依靠人工方法的開發(fā)狀態(tài)。因此，傳統(tǒng)RTCA DO-178B/C標準中部分目標不再適用于MBDV情況，同時，MBDV也存在自有的特殊方法，也會存在特有的引入錯誤的可能。在本世紀初期的民機研制和適航實踐中，民航局方經常通過對MBDV補充專門的問題紀要的形式對其符合性要求進行專門的規(guī)定。為改變這種情況，在RTCA DO-178C標準修訂時專門制定了基于模型的開發(fā)和驗證補充標準。

02MBDV在民機中的應用模式

由于民機中潛在的模型多種多樣，其表達方式以及承載的設計內涵各不相同，這將造成模型在整個層次化的研制體系中發(fā)揮不同的作用。且，由于很多實際項目中，難以用一種模型完全表達一款機載軟件中所有的需求和設計，往往存在模型和文本需求/設計混用的情況。以下是幾個不同的模型場景例子：

下表提供了幾組使用了模型的軟件生命周期，解釋了不同的模型開發(fā)時的較高級需求：

表1?不同模型開發(fā)時的模型運用場景

例A:用來描述低級需求和軟件構架的模型，如表1中案例3，用一個或者多個模型來代表軟件的低級需求和軟件構架。

圖 1

例B:用來描述高級需求、低級需求和軟件構架的模型，如表1中案例2。

圖 2

例C:另一種用來描述高級需求、低級需求和軟件構架的模型。

圖 3

例D：僅用一個模型來描述部分的高級需求，其下層為經典的開發(fā)流程。

圖 4

例E：如表1中案例2，僅用一個模型來描述系統(tǒng)設計、高級需求、低級軟件需求和軟件的構架。

圖 5

03MBDV在民機適航中的主要挑戰(zhàn)

3.1層次和追溯方面的問題

傳統(tǒng)的機載軟件過程要求軟件研制環(huán)境具備明顯的層次特征，且不同層次之間實現嚴格的追溯關系。然而，由于模型的引入，傳統(tǒng)上通過條目進行的追溯方法變得困難。且，由于不同類型的模型表達的需求和設計維度不同，模型在層次中的定位實際上無法給出統(tǒng)一的規(guī)定，進一步加劇了上述問題。具體在運用過程中，由于模型中的單元維度與傳統(tǒng)條目化需求和設計中的維度不同，研制單位可能難以建立有效的精確追溯，或者難以檢查和評估追溯的正確和完整性。此外，由于層次的相對不穩(wěn)定，也造成了模型具體需要滿足機載軟件適航標準中哪些生命周期目標變得不再直接。

3.2 模型仿真方法的有效性

在早期開展模型化設計的研制單位內，模型自身可以通過早期的仿真來檢驗設計的正確性是模型運用的重要驅動力。相比于必須完成代碼開發(fā)和集成才能通過測試檢驗正確性的傳統(tǒng)開發(fā)環(huán)境，仿真方法無疑將早期驗證活動很大程度上自動化了。然而，作為民機軟件工程，為保證產品的安全性，驗證方法自身的有效性也是重要的方面。在通用軟件中使用的很多技術，由于難以達到民機適航所要求的確定性和準確性水平，難以在民機中使用的例子屢見不鮮。為此，使用模型仿真的研制單位，需要在定義模型以及設計模型仿真方法的過程中，通過理論分析以及實踐檢驗等方法自證模型仿真的有效性。這也無疑提高了在民機中運用模型方法的難度。

04標準中對MBDV的要求

DO-331標準，正是基于上述兩點，對使用模型定義的各級需求/架構/設計數據的研制和驗證要求（包括驗證覆蓋率的判斷方法）、仿真作為驗證手段的符合性要求進行了規(guī)定。

在具體工程應用中，利用基于模型的方法進行機載軟件的研制和驗證時，除了要滿足DO-178C中相應過程的目標外，還需要滿足補充文件DO-331中新增的如下幾類目標。

（1）軟件開發(fā)過程

·標識任何對高級需求實現或執(zhí)行無用的特定模型元件

當軟件高級需求可以通過規(guī)范模型進行表示時，沒有描述任何高級需求且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應該被標識出來。該目標是否滿足可以通過MB.6.3.1中的驗證目標進行證明。

·標識任何對軟件架構實現或執(zhí)行無用的設計模型元件

當軟件低級需求可以通過規(guī)范模型進行表示時，沒有描述任何低級需求且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應該被標識出來。該目標是否滿足可以通過MB.6.3.2中的驗證目標進行證明。

·標識任何對低級需求實現或執(zhí)行無用的設計模型元件

當軟件架構可以通過規(guī)范模型進行表示時，沒有描述任何軟件架構且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應該被標識出來。該目標是否滿足可以通過MB.6.3.3中的驗證目標進行證明。

（2）軟件需求過程輸出結果的驗證

·仿真用例正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-3中目標1、2、4或7是否滿足，則在傳統(tǒng)測試方法的基礎上必須補充對仿真用例的確認工作。MB.A-7目標10“仿真用例正確”也應被滿足。

·仿真程序正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-3中目標1、2、4或7是否滿足，則目標“仿真程序正確”也應被滿足。

·仿真結果正確，并且解釋差異性

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-3中目標1、2、4或7是否滿足，則目標“仿真結果正確，并且解釋差異性”也應被滿足。

（3）軟件設計過程輸出結果的驗證

·仿真用例正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-4中目標1、2、4、7、8、9或11是否滿足，則目標“仿真用例正確”也應被滿足。

·仿真程序正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-4中目標1、2、4、7、8、9或11是否滿足，則目標“仿真程序正確”也應被滿足。

·仿真結果正確，并且解釋差異性

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-3中目標1、2、4、7、8、9或11是否滿足，則目標“仿真結果正確，并且解釋差異性”也應被滿足。

（4）軟件驗證過程輸出結果的驗證

·仿真用例正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-6中目標1或2是否滿足，則目標“仿真用例正確”也應被滿足。

·仿真程序正確

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-6中目標1或2是否滿足，則目標“仿真程序正確”也應被滿足。

·仿真結果正確，并且解釋差異性

補充文件DO-331中規(guī)定，若使用仿真技術作為符合性方法，用于證明表格MB.A-6中目標1或2是否滿足，則目標“仿真結果正確，并且解釋差異性”也應被滿足。

審核編輯：湯梓紅