本文作為#嵌入式系統(tǒng)Ansys SCADE系列專題內(nèi)容，此次將主要介紹『基于SCADE Suite模型的驗(yàn)證』，第一部分是關(guān)于驗(yàn)證手段的介紹，其中包含Ansys SCADE Suite支持的驗(yàn)證工具介紹；第二部分是介紹如何使用SCADE認(rèn)證級測試環(huán)境；第三至第七部分是其他驗(yàn)證手段的介紹。

《安全關(guān)鍵軟件開發(fā)與審定—DO-178C標(biāo)準(zhǔn)實(shí)踐指南》書中指出：驗(yàn)證，是應(yīng)用于整個軟件生命周期的一個整體性過程。在DO-178C中的驗(yàn)證，是包括評審、分析和測試的一個組合。評審是提供一個定性的評估；分析是提供正確性的可重復(fù)的證據(jù)；測試是運(yùn)行一個系統(tǒng)或系統(tǒng)部件，以驗(yàn)證它滿足指定的需求并檢測其錯誤。

《基于模型的開發(fā)和驗(yàn)證標(biāo)準(zhǔn)—DO-331》中指出使用基于模型的開發(fā)和驗(yàn)證(MBDV)后，就在傳統(tǒng)驗(yàn)證手段基礎(chǔ)上增加了模型仿真。模型仿真指使用仿真器檢查一個模型行為的活動，模型仿真器是一個設(shè)備、計算機(jī)程序或系統(tǒng)，使得一個模型能夠執(zhí)行以表明其行為，從而支持驗(yàn)證確認(rèn)。DO-178C中原先通常由評審，分析和測試完成的驗(yàn)證工作，可以由模型仿真部分來代替或者組合進(jìn)行。具體驗(yàn)證流程中使用的關(guān)于模型仿真的方法，需要寫入驗(yàn)證計劃并通過局方的審查，DO-331提供了模型仿真的專門指南。

針對軟件高層需求、軟件低層需求、軟件架構(gòu)這些數(shù)據(jù)，相對于評審和分析的傳統(tǒng)手段，模型仿真是一種動態(tài)的驗(yàn)證手段，更加直觀有效。模型仿真的主要特點(diǎn)是：

• 測試是針對可執(zhí)行目標(biāo)碼來進(jìn)行的，模型仿真主要是針對低層需求(設(shè)計模型和軟件架構(gòu))的仿真；

• 大部分模型仿真工具使用的代碼通常不同于加載到目標(biāo)環(huán)境的代碼；

• 模型仿真的環(huán)境通常是PC，也不同于測試使用的目標(biāo)機(jī)運(yùn)行環(huán)境。

所以，使用模型仿真依然不能省略在目標(biāo)機(jī)上的測試活動。DO-331的MB.6.8.3節(jié)指出：模型是基于需求開發(fā)出來的，為模型仿真而開發(fā)的仿真用例和仿真規(guī)程，也應(yīng)該是基于同樣的需求編寫的。考察DO-178C的流程，Suite模型通常相當(dāng)于低層需求，則Suite模型、仿真用例和仿真規(guī)程都是基于高層需求設(shè)計的。如果仿真用例和仿真規(guī)程用于正式驗(yàn)證置信度，那么，仿真用例和仿真規(guī)程的準(zhǔn)確性需要驗(yàn)證，仿真結(jié)果需要評審，仿真結(jié)果與預(yù)期結(jié)果的差異需要解釋。

SCADE模型檢查器 (Model Checker) 支持靜態(tài)檢查Suite模型的語法語義，這是最基本的驗(yàn)證活動，也是成功運(yùn)行其他SCADE驗(yàn)證工具和方法的前提。它通過一組內(nèi)置的規(guī)則檢查SCADE模型，檢查完畢后生成報告，其中包含檢測到的可能的警告或錯誤。其主要功能是檢查1.丟失的或多余的定義；2類型一致性；3. 時序一致性；4. 因果分析的一致性；5. 初始化分析一致性等規(guī)則。

SCADE模型仿真器 (Model Simulation) 支持在PC端仿真模型的行為，也可以作為QTE大規(guī)模自動化模型仿真活動之前的預(yù)仿真。SCADE 仿真器是可視化的調(diào)試環(huán)境，支持?jǐn)帱c(diǎn)設(shè)定，測試用例的保存、載入、測試結(jié)果的輸出等功能完成模型仿真。

SCADE認(rèn)證級測試環(huán)境 (Qualified Test Environment) 是一套自動化環(huán)境，除融合了模型仿真和模型覆蓋驗(yàn)證功能外，還支持管理仿真用例、仿真規(guī)程和仿真結(jié)果。

SCADE模型覆蓋分析 (Model Coverage) 支持低層需求的覆蓋驗(yàn)證。除了可以單獨(dú)執(zhí)行外，更常見的操作是基于QTE進(jìn)行大規(guī)模自動化的模型覆蓋。

以上四個工具可應(yīng)用于SCADE開發(fā)安全關(guān)鍵項(xiàng)目中最基本的驗(yàn)證活動。除此之外，還有SCADE快速原型(Rapid Prototype)，SCADE形式化驗(yàn)證(Design Verify)（*關(guān)于該部分內(nèi)容可詳細(xì)參考《基于SCADE模型的形式化方法》的第五節(jié)），SCADE最壞運(yùn)行時間和堆棧分析(Timing and Stack Optimizer)，SCADE編譯器驗(yàn)證套件(Complier Verification Kit)，SCADE軟件生命周期管理(ALM)橋接器和SCADE多學(xué)科仿真文件生成(FMI/FMU)生成器等工具用于其他的驗(yàn)證活動。

圖表1: SCADE認(rèn)證級測試環(huán)境工作流

大規(guī)模的自動化驗(yàn)證活動推薦使用SCADE的認(rèn)證級測試環(huán)境(Qualified Test Environment)來操作。SCADE QTE是可通過DO-330 TQL-5級別鑒定的驗(yàn)證工具。SCADE QTE工作流，主要分為如下個步驟

• 驗(yàn)證軟件需求的正確性；

• 基于需求創(chuàng)建測試用例，并評審其正確性；

• 執(zhí)行在主機(jī)上的功能測試；

• 執(zhí)行在主機(jī)上的模型覆蓋分析；

• 執(zhí)行在主機(jī)上的代碼結(jié)構(gòu)覆蓋分析(SCADE 2020版本后省略該步驟)；

• 執(zhí)行在目標(biāo)機(jī)上的測試。

SCADE Suite模型最常用的測試用例類型是擴(kuò)展名為.sss的文件，該文件基于Tcl腳本格式的仿真文件格式，可擴(kuò)展性強(qiáng)。其主要的語法規(guī)則如下:

• #符號開頭的是注釋，如圖表2所示，可根據(jù)預(yù)定義的驗(yàn)證計劃編寫

• 當(dāng)前測試用例的名稱

• 當(dāng)前測試用例的描述，目標(biāo)，約束等信息

• 當(dāng)前測試用例的編號，供可追蹤性管理

• 當(dāng)前測試用例所覆蓋的上層需求編號，供可追蹤性管理

• SSM::set<var><val>

• var為輸入變量、外部引用變量 (Sensor)的名稱

• val為下一周期的輸入值

• SSM::cycle [<integer>]

• 設(shè)置運(yùn)行integer個周期

• integer為整型，數(shù)組必須大于0

• 不填寫integer，則默認(rèn)值為1

• SSM::set_tolerance [path=<var>] real=<tolerance>

• var為期望觀察的輸出變量、局部變量的名稱；

• tolerance為設(shè)置的檢測精度值。一旦設(shè)置后，該變量的檢測精度保持不變，直到有新的設(shè)置改變檢測精度。

• l SSM::ccheck <var><val> {{ sustain=(( forever | <integer> )) |real=<tolerance> }}

• integer為整型，必須大于0；

• var為待檢測的輸出、局部變量的名稱或別名；

• 該檢測語句在下一次SSM::cycle語句執(zhí)行時啟用。如果SSM::cycle語句的周期值為N且N>1，則默認(rèn)情況下，該檢測語句僅在第一周期執(zhí)行，后N-1周期不執(zhí)行；如果要檢測語句保持多執(zhí)行若干周期，可以使用sustain=……語句設(shè)置；

• 如果forever代替integer，則變量的檢測保持到測試結(jié)束；

• 如果沒有sustain=……的語句，則該變量的檢測僅在下一周期啟用；

• 該語句的real=……檢測精度設(shè)置優(yōu)先級高于SSM::set_tolerance……語句的設(shè)置；如果沒有real=……的語句，或者該語句執(zhí)行完畢后，該浮點(diǎn)型變量的檢測精度值遵從SSM::set_tolerance語句的設(shè)定；

• 初始化文件內(nèi)禁用該語句。

下圖是測試用例規(guī)則的范例

圖表2: SCADE測試用例范例

從SCADE 2020版本開始，測試用例腳本語言新增了一些擴(kuò)展，以支持用戶更好地設(shè)計測試用例

2.1.1  輸出參數(shù)支持使用Lambda表達(dá)式來檢查范圍

Lambda 表達(dá)式 (lambda expression) 支持以匿名函數(shù)形式編寫測試用例中的輸出參數(shù)

圖表3: 測試用例的輸出參數(shù)支持使用Lambda表達(dá)式

2.1.2  輸出參數(shù)支持使用區(qū)間表達(dá)式來檢查范圍

區(qū)間表達(dá)式中，可取邊界值用[]符號，不可取邊界值用][符號，注意不是用()符號

圖表4: 測試用例的輸出參數(shù)支持使用區(qū)間表達(dá)式

2.1.3  輸入輸出參數(shù)支持直接使用模型中的常量來設(shè)置

圖表5: 測試用例的輸入輸出參數(shù)支持使用模型中的常量

2.1.4  輸入輸出參數(shù)支持IEEE754標(biāo)準(zhǔn)定義的無窮數(shù)Inf和非數(shù)值Nan的使用

圖表6: 測試用例的輸入輸出參數(shù)支持IEEE754標(biāo)準(zhǔn)定義的無窮數(shù)Inf和非數(shù)值Nan

2.1.5  輸入輸出支持對字符串的某字符進(jìn)行單獨(dú)設(shè)置

圖表7: 測試用例的輸入輸出參數(shù)支持設(shè)置字符串的某單獨(dú)字符

使用SCADE QTE在主機(jī)上進(jìn)行功能測試的結(jié)果如下圖，既有圖形化的報告，也有文本化的報告。圖形化的報告既有按照測試場景周期排列的，也有按照圖形比對結(jié)果排列的。可以從結(jié)果報告中看到測試用例編號、待測變量名稱、實(shí)際輸出、期望輸出、精度約束等信息。

圖表8: 使用SCADE QTE在主機(jī)上進(jìn)行功能測試

2.3 執(zhí)行在主機(jī)上的模型覆蓋分析

《基于模型的開發(fā)和驗(yàn)證標(biāo)準(zhǔn)—DO-331》中指出模型覆蓋分析支持檢測和解決

• 基于需求的仿真用例或仿真規(guī)程的缺陷

• 高層需求的不充分或缺陷，而設(shè)計模型是基于高層需求的

• 先前未確認(rèn)的派生的低層需求

• 設(shè)計模型中的非激活功能

• 設(shè)計模型中的非預(yù)期功能

《安全關(guān)鍵軟件開發(fā)與審定—DO-178C標(biāo)準(zhǔn)實(shí)踐指南》中指出代碼結(jié)構(gòu)覆蓋分析支持檢測和解決

• 基于需求的仿真用例或仿真規(guī)程的缺陷

• 需求的不充分

• 非激活代碼

• 死代碼

另外，覆蓋分析需要依據(jù)不同的軟件研制級別選擇特定的覆蓋準(zhǔn)則。DO-178C中定義了以下幾個準(zhǔn)則：

• 語句覆蓋：設(shè)計若干測試用例，運(yùn)行被測程序，使得程序中每個可執(zhí)行語句至少執(zhí)行一次。語句覆蓋被認(rèn)為是相對較弱的準(zhǔn)則，因?yàn)樗辉u價一些控制結(jié)構(gòu)并且不檢測某種類型的邏輯錯誤。一個if-else構(gòu)造只需要判定為真，就可以達(dá)到語句覆蓋

• 判定覆蓋：設(shè)計若干測試用例，運(yùn)行被測程序，使得程序中每個判斷取真分支和取假分支至少執(zhí)行一次

• 條件變更/判定覆蓋：對每一個程序模塊的入口點(diǎn)和出口點(diǎn)都至少考慮被調(diào)用一次，且需求中的每條輸入值都至少能獨(dú)立地影響輸出值一次。航空的機(jī)載軟件領(lǐng)域僅A級軟件需要應(yīng)用該準(zhǔn)則

• 數(shù)據(jù)耦合：兩個模塊彼此間通過數(shù)據(jù)參數(shù)交換信息

• 控制耦合：模塊間傳遞的不但有數(shù)據(jù)，還包括控制信息，使得一個軟件模塊影響另外一個軟件模塊執(zhí)行的方式和程度

使用SCADE軟件進(jìn)行MBDV開發(fā)時，僅需設(shè)計一套基于高層需求的仿真用例和仿真規(guī)程，即可同時應(yīng)用于設(shè)計模型的覆蓋分析、代碼結(jié)構(gòu)的覆蓋分析。

圖表9: 基于高層需求的仿真用例可以同時進(jìn)行模型覆蓋分析和代碼結(jié)構(gòu)覆蓋分析

SCADE MTC是可通過DO-330 TQL-5級別鑒定的驗(yàn)證工具。程序插樁(Instrument)是覆蓋分析的關(guān)鍵技術(shù)之一，它是在保證被測程序原有邏輯完整性的基礎(chǔ)上插入一些探針(本質(zhì)上就是進(jìn)行信息采集的代碼段，可以是賦值語句或采集覆蓋信息的函數(shù)調(diào)用) ，通過探針的執(zhí)行并拋出程序運(yùn)行的特征數(shù)據(jù)，通過對這些數(shù)據(jù)的分析，可以獲得程序的控制流和數(shù)據(jù)流信息，進(jìn)而得到邏輯覆蓋等動態(tài)信息，從而實(shí)現(xiàn)測試目的的方法。SCADE同樣使用插樁技術(shù)進(jìn)行覆蓋分析, SCADE MTC在2019版本之前是可通過DO-178C/DO-330 TQL-5級別鑒定的驗(yàn)證工具。

使用SCADE QTE在主機(jī)上進(jìn)行模型覆蓋分析結(jié)果如下圖，可以便捷地通過顏色來區(qū)分覆蓋分析的完整度，綠色是完全覆蓋，黃色是部分覆蓋，紅色是未覆蓋。

圖表10: 使用SCADE QTE在主機(jī)上進(jìn)行模型覆蓋分析

2.3.1  模型覆蓋分析的新特性

從SCADE 2019版本開始，SCADE Suite的覆蓋分析工具經(jīng)過改進(jìn)提升，可通過DO-178C/DO-331 TQL-4級鑒定，因此在一定條件下，使用該工具進(jìn)行的模型覆蓋分析也等價于代碼結(jié)構(gòu)覆蓋分析。

而在結(jié)構(gòu)覆蓋點(diǎn)不充分時，支持使用預(yù)定義的定制操作符進(jìn)行覆蓋分析。定制覆蓋方法中需要區(qū)分出覆蓋觀察操作符(CO: Coverage Observer)和被觀察操作符(Observee)，覆蓋觀察操作符CO需要將被觀察操作符的所有I/O都作為輸入，根據(jù)覆蓋觀察操作符CO的輸出不同，分為三種定制覆蓋情況。

2.3.1.1       覆蓋觀察操作符CO無輸出

圖表11: 定制模型覆蓋分析情況一，CO無輸出

2.3.1.2       覆蓋觀察操作符CO僅返回一個輸出

圖表12: 定制模型覆蓋分析情況二，CO僅返回一個輸出

2.3.1.3       覆蓋觀察操作符CO返回與被觀察操作符同樣多的輸出

圖表13: 定制模型覆蓋分析情況三，CO返回若干個輸出

2.3.2  使用形式化分析引擎協(xié)助進(jìn)行模型覆蓋分析

作為完整的驗(yàn)證活動的一部分, 覆蓋分析總是最耗時的。在大型認(rèn)證級項(xiàng)目中，工程師們很難對某些嵌套關(guān)系或者組合關(guān)系特別復(fù)雜的分支快速便捷地設(shè)計出對應(yīng)的測試用例，以分析出該未覆蓋的分支到底是：

• 測試用例不足引起的

• 還是死/未激活代碼引起的

SCADE Suite從2021版本開始推出使用形式化方法來協(xié)助分析模型覆蓋結(jié)果，該方法可以極大地減少工程師們在模型覆蓋分析活動中的工作量，在國內(nèi)航空航天、軌道交通幾家單位的試點(diǎn)應(yīng)用后反饋良好。該方法的原理可參考《基于SCADE模型的形式化方法》中第六節(jié)的內(nèi)容。通常該方法的分析結(jié)果有三種

• 可覆蓋Coverable : 返回測試用例(.sss類型)

• 不可覆蓋Uncoverable : 證明該分支不可達(dá)

• 未知Undecided : 在指定條件下因狀態(tài)空間暴漲使得形式化分析引擎無解

該方法既可以在模型開發(fā)階段使用，也可以在模型的驗(yàn)證階段使用。為了縮小分析的狀態(tài)空間，該方法同樣支持在模型中添加包括Assume和Guarantee在內(nèi)的約束,使得形式化分析引擎在限定的范圍內(nèi)得出有意義的結(jié)果。

使用老版本SCADE軟件的用戶也可以通過升級軟件并使用該功能來積累測試用例，然后退回到老版本SCADE中復(fù)用先前積累的測試用例進(jìn)行覆蓋分析。值得一提的是，推導(dǎo)出來的測試用例需要進(jìn)行評審或分析，補(bǔ)充可能的高層需求。

2.3.2.1       在開發(fā)階段使用形式化方法對模型的覆蓋分析

在開發(fā)階段對模型的覆蓋分析，有助于設(shè)計人員自主分析出所設(shè)計的模型是否有非預(yù)期的不可達(dá)分支，提前改正可能的錯誤，以減輕后期驗(yàn)證階段測試人員覆蓋分析的工作量。使用方法是在開發(fā)工程中，右鍵單擊某操作符，在彈出菜單中選擇Coverability Analysis->Analyze，等待片刻后(模型越復(fù)雜等待時間越長)，會得出分析結(jié)果。如果分支可以覆蓋，條目的背景色為綠色，Result列顯示COVERABLE，并在最后一列返回出可覆蓋該分支的測試用例的文件路徑超鏈接，可點(diǎn)擊該超鏈接打開該文件。如果分支不可覆蓋，條目的背景色為紅色，Result列顯示NOT COVERABLE，且最后一列為空。

圖表14: 在開發(fā)階段使用形式化方法對模型的覆蓋分析，結(jié)果可覆蓋

圖表15: 在開發(fā)階段使用形式化方法對模型的覆蓋分析，結(jié)果不可覆蓋

2.3.2.2       在驗(yàn)證階段使用形式化方法對模型的覆蓋分析

在驗(yàn)證階段對模型的覆蓋分析操作方法是先做完2.3節(jié)主機(jī)上的模型覆蓋分析后，針對驗(yàn)證工程中未覆蓋的分支，右鍵單擊某分支未完全覆蓋的操作符，在彈出菜單中選擇Coverability Analysis->Analyze，等待片刻后(模型越復(fù)雜等待時間越長)，會得出分析結(jié)果。

圖表16: 在驗(yàn)證階段使用形式化方法對模型的覆蓋分析

如2.3節(jié)所述，在SCADE 2019版本之前，SCADE Suite 覆蓋分析工具僅可通過DO-178C/DO-331 TQL-5級工具鑒定，因此需要進(jìn)行模型覆蓋分析和代碼覆蓋分析兩項(xiàng)驗(yàn)證活動。而在在SCADE 2019版本之后，SCADE Suite覆蓋分析工具可通過DO-178C/DO-331 TQL-4級鑒定，因此在一定條件下，使用該工具進(jìn)行的模型覆蓋分析等價于代碼結(jié)構(gòu)覆蓋分析。如果用戶使用的是老版本的SCADE工具，依然可以通過單擊代碼分析按鈕的操作，獲取模型對應(yīng)的代碼級覆蓋分析結(jié)果。

圖表17: 使用SCADE QTE在主機(jī)上進(jìn)行代碼覆蓋分析

如果需要在目標(biāo)機(jī)上進(jìn)行軟硬件集成測試時，SCADE QTE支持將主機(jī)上測試完畢后得到的測試用例轉(zhuǎn)換為可連接目標(biāo)機(jī)的第三方程序?qū)?yīng)的測試用例，以便用戶能簡單快捷地進(jìn)行目標(biāo)機(jī)上的測試。SCADE QTE可支持向LDRA Test，IBM RTRT，VectorCast，CANTAT和RapiTest等多款軟件的測試用例轉(zhuǎn)換。

圖表18: 使用SCADE QTE在目標(biāo)機(jī)上的測試

SCADE快速原型 (Rapid Prototype) 支持快速設(shè)計人機(jī)界面，可用于和SCADE Suite模型的接口映射后，進(jìn)行交互式驗(yàn)證或直接生成獨(dú)立可執(zhí)行程序。

圖表19: SCADE快速原型 (Rapid Prototype) 設(shè)計的人機(jī)界面

SCADE嵌入了AbsInt公司的aiT WCET和StackAnalyzer兩個工具，并在此基礎(chǔ)上定制形成了SCADE Suite TSO/TSV (Timing and Stack Optimizer/Verifier) 兩款工具，使得用戶可基于Suite模型直接進(jìn)行性能分析，以滿足DO-178C中目標(biāo)機(jī)兼容方面的分析工作。aiT WCET和StackAnalyzer兩款工具的詳細(xì)介紹可參考安裝目錄下AbsInt公司的手冊。

圖表20: SCADE Suite運(yùn)行最壞運(yùn)行時間和堆棧分析的工作流

在安全關(guān)鍵項(xiàng)目的開發(fā)中，SCADE編譯器驗(yàn)證套件主要有兩大作用

1.CVK支持驗(yàn)證編譯器

• 在特定的嵌入式操作系統(tǒng)（Embedded OS）上

• 在特定的中央處理器（CPU）上

• 在特定的編譯選項(xiàng)（Compiler Option）上

是否可以將SCADE Suite KCG生成的C代碼正確地編譯為目標(biāo)碼。

2.在項(xiàng)目前期通過使用CVK后，以極小的工作量就可以得出目標(biāo)機(jī)兼容相關(guān)的限制信息。可在此基礎(chǔ)上定制Suite建模規(guī)范，完善DO-178C標(biāo)準(zhǔn)的計劃過程中的開發(fā)標(biāo)準(zhǔn)。另外，也可以設(shè)計專門的規(guī)則檢查器，以檢測設(shè)計的模型是否違反了定制的建模規(guī)范。

編譯器驗(yàn)證包主要包括如下內(nèi)容

• C語言的安全子集

• 符合上述C語言安全子集的樣本代碼，即參考C代碼

• 參考C代碼達(dá)到100%MC/DC覆蓋的測試用例

• 基于PC機(jī)的自動化測試腳本

• 相關(guān)幫助支持文檔

圖表21: 編譯器驗(yàn)證包結(jié)構(gòu)圖

DO-178C標(biāo)準(zhǔn)的5.5節(jié)描述了軟件開發(fā)過程的可追蹤性要求：

應(yīng)建立系統(tǒng)需求和高層需求之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 驗(yàn)證系統(tǒng)需求是否被完整地實(shí)現(xiàn)；

• 直觀地看出無法追蹤到系統(tǒng)需求的派生高層需求。

應(yīng)建立低層需求和高層需求之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 驗(yàn)證高層需求是否被完整地實(shí)現(xiàn)；

• 直觀地看出無法追蹤到高層需求和架構(gòu)設(shè)計的派生低層需求。

應(yīng)建立低層需求和源代碼之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 驗(yàn)證低層需求是否被完整地實(shí)現(xiàn)

• 驗(yàn)證是否存在非預(yù)期的源代碼；

DO-178C標(biāo)準(zhǔn)的6.5節(jié)主要描述軟件驗(yàn)證過程的可追蹤性要求：

應(yīng)建立軟件需求和測試用例之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 支持基于需求的測試覆蓋分析。

應(yīng)建立測試用例和測試規(guī)程之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 驗(yàn)證測試用例被完整地開發(fā)成測試規(guī)程了。

應(yīng)建立測試規(guī)程和測試結(jié)果之間的雙向可追蹤性，以便能完成以下功能和目標(biāo)。

• 驗(yàn)證測試規(guī)程是否被完整地執(zhí)行了

SCADE軟件生命周期管理 (ALM: Application Lifecycle Management) 橋接器支持與第三方ALM工具連接起來，將SCADE Architect架構(gòu)模型，SCADE Suite控制模型，SCADE Display人機(jī)界面模型，SCADE Test測試用例與高層需求進(jìn)行雙向追蹤，幫助用戶管理需求、模型、測試用例、測試規(guī)程等和其他結(jié)構(gòu)化文檔之間的追蹤關(guān)系。SCADE當(dāng)前支持橋接的第三方ALM工具包括Reqtify，DORRS 9.6+(Native)，DOORS Next Generation，Jama和Polarion等。

圖表22: SCADE軟件生命周期管理 (ALM)橋接器的簡易操作方法

FMI標(biāo)準(zhǔn)的全稱是Functional Mock-up Interface，是一個不依賴于工具的標(biāo)準(zhǔn)，其通過XML文件和已編譯的C代碼的組合來同時支持動態(tài)模型的模型交換 (Model Exchange) 和聯(lián)合仿真 (Co-Simulation) 。兩者的區(qū)別是模型交換方法導(dǎo)出的FMU文件不包含求解模型方程的求解器，而聯(lián)合仿真方法導(dǎo)出的FMU文件包含求解模型方程的求解器。即是否包含求解器是兩者最大的區(qū)別。

由于FMI標(biāo)準(zhǔn)是一個通用的第三方接口標(biāo)準(zhǔn)，不依賴于任何工具特有的接口形式。所以，只要是支持FMI標(biāo)準(zhǔn)的工具都可以將其他工具導(dǎo)出的FMU文件導(dǎo)入到自身的軟件平臺內(nèi)，這時仿真軟件會自動解析FMU中的.xml文件，并在軟件的操作界面上給用戶提供操作FMU的選項(xiàng)。

SCADE多學(xué)科仿真文件生成 (FMI/FMU) 支持將SCADE模型導(dǎo)出為FMU文件后，再導(dǎo)入到多學(xué)科仿真平臺中進(jìn)行系統(tǒng)級仿真。

[1] Leanna Rierson．安全關(guān)鍵軟件開發(fā)與審定——DO-178C 標(biāo)準(zhǔn)實(shí)踐指南[M]．崔曉峰譯．北京：電子工業(yè)出版社，2015．

[2] 蔡喁，鄭征，蔡開元，等．機(jī)載軟件適航標(biāo)準(zhǔn)DO-178B/C 研究[M]．上海：上海交通大學(xué)出版社，2013．

[3] DO-178C.Software Considerations in Airborne Systems and Equipment Certification[S]. December 13, 2011．

[4] RTCA (Firm). SC-205, EUROCAE (Agency). Working Group 71. Model-based Development and Verification Supplement to DO-178C and DO-278A[M]. RTCA, Incorporated, 2011．