基于模型的方法在民機機載軟件中的應(yīng)用

作者 | 蔡喁上?？匕部尚跑浖?chuàng)新研究院副院長

版塊 |鑒源論壇 · 觀擎

社群 |添加微信號“TICPShanghai”加入“上海控安51fusa安全社區(qū)”

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

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

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

2.該模型包含軟件需求和/或軟件體系結(jié)構(gòu)定義。

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

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

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

02MBDV在民機中的應(yīng)用模式

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

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

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

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

圖 1

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

圖 2

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

圖 3

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

圖 4

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

圖 5

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

3.1層次和追溯方面的問題

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

3.2 模型仿真方法的有效性

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

04標(biāo)準(zhǔn)中對MBDV的要求

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

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

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

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

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

·標(biāo)識任何對軟件架構(gòu)實現(xiàn)或執(zhí)行無用的設(shè)計模型元件

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

·標(biāo)識任何對低級需求實現(xiàn)或執(zhí)行無用的設(shè)計模型元件

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

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

·仿真用例正確

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

·仿真程序正確

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

·仿真結(jié)果正確，并且解釋差異性

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

（3）軟件設(shè)計過程輸出結(jié)果的驗證

·仿真用例正確

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

·仿真程序正確

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

·仿真結(jié)果正確，并且解釋差異性

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

（4）軟件驗證過程輸出結(jié)果的驗證

·仿真用例正確

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

·仿真程序正確

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

·仿真結(jié)果正確，并且解釋差異性

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

審核編輯：湯梓紅