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

版塊 |鑒源論壇 · 觀擎

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

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

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

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

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

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

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

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

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

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

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

表1?不同模型開發(fā)時(shí)的模型運(yùn)用場(chǎng)景

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

圖 1

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

圖 2

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

圖 3

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

圖 4

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

圖 5

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

3.1層次和追溯方面的問(wèn)題

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

3.2 模型仿真方法的有效性

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

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

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

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

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

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

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

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

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

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

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

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

·仿真用例正確

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

·仿真程序正確

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

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

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

（3）軟件設(shè)計(jì)過(guò)程輸出結(jié)果的驗(yàn)證

·仿真用例正確

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

·仿真程序正確

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

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

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

（4）軟件驗(yàn)證過(guò)程輸出結(jié)果的驗(yàn)證

·仿真用例正確

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

·仿真程序正確

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

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

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

審核編輯：湯梓紅