作者 | 蔡喁上??匕部尚跑浖?chuàng)新研究院副院長
版塊 |鑒源論壇 · 觀擎
社群 |添加微信號“TICPShanghai”加入“上海控安51fusa安全社區(qū)”
01基于模型的開發(fā)和驗(yàn)證MBDV
模型泛指用于支持軟件開發(fā)過程或軟件驗(yàn)證過程的系統(tǒng)的一組軟件方面的抽象表示,在機(jī)載軟件中,基于模型的開發(fā)和驗(yàn)證中所涉及的模型一般包含以下特征:
1.使用明確標(biāo)識的建模符號來完全描述模型。這里所說的建模符號可以是圖形和/或文本的。
2.該模型包含軟件需求和/或軟件體系結(jié)構(gòu)定義。
3.該模型的形式和類型用于軟件開發(fā)過程或軟件再驗(yàn)證過程支持的直接分析或行為評估。
相比之下一些其他類型的“類模型方法”在機(jī)載軟件領(lǐng)域內(nèi)并不被定義為一種MBDV方法。包括無法形成語法語義有限閉環(huán)的圖形表達(dá)方法、或者在機(jī)載軟件生命周期中無法用于表達(dá)需求/設(shè)計(jì)的圖文結(jié)合表達(dá)方法。
之所以在民機(jī)機(jī)載軟件中對模型開發(fā)進(jìn)行如此的定義,與民用飛機(jī)所面臨的適航符合性要求是相關(guān)的。正如前面幾期介紹的,機(jī)載軟件適航標(biāo)準(zhǔn)對軟件研制過程、生命周期數(shù)據(jù)以及符合性證據(jù)等都提出了明確的要求。然而,這些過程要求都是建立在歐美80~90年代軟件工程實(shí)踐的基礎(chǔ)上,以文本需求+代碼為主要的開發(fā)方式。隨著近些年模型技術(shù)的進(jìn)步,很多研制方法中通過模型表達(dá)需求或者設(shè)計(jì),從而改變了以往單純依靠人工方法的開發(fā)狀態(tài)。因此,傳統(tǒng)RTCA DO-178B/C標(biāo)準(zhǔn)中部分目標(biāo)不再適用于MBDV情況,同時,MBDV也存在自有的特殊方法,也會存在特有的引入錯誤的可能。在本世紀(jì)初期的民機(jī)研制和適航實(shí)踐中,民航局方經(jīng)常通過對MBDV補(bǔ)充專門的問題紀(jì)要的形式對其符合性要求進(jìn)行專門的規(guī)定。為改變這種情況,在RTCA DO-178C標(biāo)準(zhǔn)修訂時專門制定了基于模型的開發(fā)和驗(yàn)證補(bǔ)充標(biāo)準(zhǔn)。
02MBDV在民機(jī)中的應(yīng)用模式
由于民機(jī)中潛在的模型多種多樣,其表達(dá)方式以及承載的設(shè)計(jì)內(nèi)涵各不相同,這將造成模型在整個層次化的研制體系中發(fā)揮不同的作用。且,由于很多實(shí)際項(xiàng)目中,難以用一種模型完全表達(dá)一款機(jī)載軟件中所有的需求和設(shè)計(jì),往往存在模型和文本需求/設(shè)計(jì)混用的情況。以下是幾個不同的模型場景例子:
下表提供了幾組使用了模型的軟件生命周期,解釋了不同的模型開發(fā)時的較高級需求:
表1?不同模型開發(fā)時的模型運(yùn)用場景
例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è)計(jì)、高級需求、低級軟件需求和軟件的構(gòu)架。
圖 5
03MBDV在民機(jī)適航中的主要挑戰(zhàn)
3.1層次和追溯方面的問題
傳統(tǒng)的機(jī)載軟件過程要求軟件研制環(huán)境具備明顯的層次特征,且不同層次之間實(shí)現(xiàn)嚴(yán)格的追溯關(guān)系。然而,由于模型的引入,傳統(tǒng)上通過條目進(jìn)行的追溯方法變得困難。且,由于不同類型的模型表達(dá)的需求和設(shè)計(jì)維度不同,模型在層次中的定位實(shí)際上無法給出統(tǒng)一的規(guī)定,進(jìn)一步加劇了上述問題。具體在運(yùn)用過程中,由于模型中的單元維度與傳統(tǒng)條目化需求和設(shè)計(jì)中的維度不同,研制單位可能難以建立有效的精確追溯,或者難以檢查和評估追溯的正確和完整性。此外,由于層次的相對不穩(wěn)定,也造成了模型具體需要滿足機(jī)載軟件適航標(biāo)準(zhǔn)中哪些生命周期目標(biāo)變得不再直接。
3.2 模型仿真方法的有效性
在早期開展模型化設(shè)計(jì)的研制單位內(nèi),模型自身可以通過早期的仿真來檢驗(yàn)設(shè)計(jì)的正確性是模型運(yùn)用的重要驅(qū)動力。相比于必須完成代碼開發(fā)和集成才能通過測試檢驗(yàn)正確性的傳統(tǒng)開發(fā)環(huán)境,仿真方法無疑將早期驗(yàn)證活動很大程度上自動化了。然而,作為民機(jī)軟件工程,為保證產(chǎn)品的安全性,驗(yàn)證方法自身的有效性也是重要的方面。在通用軟件中使用的很多技術(shù),由于難以達(dá)到民機(jī)適航所要求的確定性和準(zhǔn)確性水平,難以在民機(jī)中使用的例子屢見不鮮。為此,使用模型仿真的研制單位,需要在定義模型以及設(shè)計(jì)模型仿真方法的過程中,通過理論分析以及實(shí)踐檢驗(yàn)等方法自證模型仿真的有效性。這也無疑提高了在民機(jī)中運(yùn)用模型方法的難度。
04標(biāo)準(zhǔn)中對MBDV的要求
DO-331標(biāo)準(zhǔn),正是基于上述兩點(diǎn),對使用模型定義的各級需求/架構(gòu)/設(shè)計(jì)數(shù)據(jù)的研制和驗(yàn)證要求(包括驗(yàn)證覆蓋率的判斷方法)、仿真作為驗(yàn)證手段的符合性要求進(jìn)行了規(guī)定。
在具體工程應(yīng)用中,利用基于模型的方法進(jìn)行機(jī)載軟件的研制和驗(yàn)證時,除了要滿足DO-178C中相應(yīng)過程的目標(biāo)外,還需要滿足補(bǔ)充文件DO-331中新增的如下幾類目標(biāo)。
(1)軟件開發(fā)過程
·標(biāo)識任何對高級需求實(shí)現(xiàn)或執(zhí)行無用的特定模型元件
當(dāng)軟件高級需求可以通過規(guī)范模型進(jìn)行表示時,沒有描述任何高級需求且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應(yīng)該被標(biāo)識出來。該目標(biāo)是否滿足可以通過MB.6.3.1中的驗(yàn)證目標(biāo)進(jìn)行證明。
·標(biāo)識任何對軟件架構(gòu)實(shí)現(xiàn)或執(zhí)行無用的設(shè)計(jì)模型元件
當(dāng)軟件低級需求可以通過規(guī)范模型進(jìn)行表示時,沒有描述任何低級需求且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應(yīng)該被標(biāo)識出來。該目標(biāo)是否滿足可以通過MB.6.3.2中的驗(yàn)證目標(biāo)進(jìn)行證明。
·標(biāo)識任何對低級需求實(shí)現(xiàn)或執(zhí)行無用的設(shè)計(jì)模型元件
當(dāng)軟件架構(gòu)可以通過規(guī)范模型進(jìn)行表示時,沒有描述任何軟件架構(gòu)且不能作為開發(fā)過程或開發(fā)活動輸入的模型元件都應(yīng)該被標(biāo)識出來。該目標(biāo)是否滿足可以通過MB.6.3.3中的驗(yàn)證目標(biāo)進(jìn)行證明。
(2)軟件需求過程輸出結(jié)果的驗(yàn)證
·仿真用例正確
補(bǔ)充文件DO-331中規(guī)定,若使用仿真技術(shù)作為符合性方法,用于證明表格MB.A-3中目標(biāo)1、2、4或7是否滿足,則在傳統(tǒng)測試方法的基礎(chǔ)上必須補(bǔ)充對仿真用例的確認(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ì)過程輸出結(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)證過程輸出結(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)被滿足。
審核編輯:湯梓紅
-
仿真
+關(guān)注
關(guān)注
50文章
3995瀏覽量
133228 -
軟件
+關(guān)注
關(guān)注
69文章
4617瀏覽量
86995 -
模型
+關(guān)注
關(guān)注
1文章
3062瀏覽量
48575
發(fā)布評論請先 登錄
相關(guān)推薦
評論