您如何建立對(duì)用于安全關(guān)鍵系統(tǒng)的自動(dòng)代碼生成器的信任？例如，給定一個(gè)代碼生成器，它采用 Simulink 和 Stateflow 中表示的飛行控制系統(tǒng)的實(shí)時(shí)模型，并將其轉(zhuǎn)換為 MISRA C 或 Ada 的 SPARK 子集，哪個(gè)過程可以確保生成的代碼是原始實(shí)時(shí)模型的忠實(shí)表示？美國(guó)聯(lián)邦航空管理局 （FAA） 有一個(gè)定義明確的流程來(lái)創(chuàng)建合格的代碼生成器，這意味著一個(gè)代碼生成器，其輸出可以信任為與輸入模型的語(yǔ)義完全匹配，沒有遺漏任何內(nèi)容，也沒有添加任何內(nèi)容。此過程在 DO-178C（機(jī)載系統(tǒng)中的軟件注意事項(xiàng)）及其隨附的文檔 DO-330（軟件工具認(rèn)證注意事項(xiàng)）和 DO-331（基于模型的開發(fā)和驗(yàn)證）中定義。

對(duì)于像代碼生成器這樣的工具，可能會(huì)將錯(cuò)誤插入機(jī)載系統(tǒng)，如果要將工具用于故障可能是災(zāi)難性的子系統(tǒng)（A 級(jí)子系統(tǒng)），則需要最高級(jí)別的工具資格（工具資格級(jí)別 1 （TQL-1））。

毫不奇怪，這種級(jí)別的工具鑒定可能涉及大量的時(shí)間和精力，通常估計(jì)為每 1，000 行代碼 （KSLOC） 數(shù)百小時(shí)。這類似于驗(yàn)證 A 級(jí)安全關(guān)鍵型嵌入式軟件組件所需的每行工作量。但是工具可以有更多的代碼行。例如，如果該工具是100 KSLOC，則傳統(tǒng)的A級(jí)驗(yàn)證方法可能花費(fèi)約500萬(wàn)美元。因此，有強(qiáng)烈的動(dòng)機(jī)研究測(cè)試此類工具的替代方法，同時(shí)仍然實(shí)現(xiàn)TQL-1目標(biāo)。

傳統(tǒng)的測(cè)試方法

驗(yàn)證高完整性應(yīng)用程序的傳統(tǒng)方法要求測(cè)試人員：

仔細(xì)定義和驗(yàn)證應(yīng)用程序的一組高級(jí)要求

從高級(jí)需求派生模塊級(jí)需求，這些要求足夠具體，可以確定適當(dāng)?shù)膶?shí)現(xiàn)

使用單元測(cè)試根據(jù)其低級(jí)需求檢查實(shí)現(xiàn)的每個(gè)模塊

對(duì)所有高級(jí)需求執(zhí)行集成級(jí)測(cè)試

然后執(zhí)行覆蓋率分析，以確保這些測(cè)試涵蓋所有代碼，并確保應(yīng)用程序中沒有可能提供額外、不需要的功能的代碼。

對(duì)于嵌入式軟件組件，每個(gè)模塊的單元級(jí)測(cè)試和整個(gè)組件的集成級(jí)測(cè)試的組合可以很好地工作。特別是，嵌入式軟件模塊的單元測(cè)試是實(shí)用的，因?yàn)樵谠S多情況下，每個(gè)模塊的輸入數(shù)量和復(fù)雜性是可管理的，并且輸出相對(duì)容易識(shí)別和檢查。但是，對(duì)于像自動(dòng)代碼生成器這樣的工具，它通常涉及多個(gè)階段，涉及將輸入模型逐步轉(zhuǎn)換為生成的代碼，單元測(cè)試可能是一個(gè)真正的挑戰(zhàn)。另一方面，對(duì)于這樣的工具來(lái)說(shuō)，集成測(cè)試并沒有明顯困難，因?yàn)橹虚g階段的數(shù)量不會(huì)影響工具的整體輸入和輸出。

圖 1 說(shuō)明了單元測(cè)試的復(fù)雜性與多階段工具（如代碼生成器）的集成測(cè)試相對(duì)容易程度之間的這種二分法。

［圖1 |由于易于使用，集成測(cè)試比單元測(cè)試更受歡迎。

在圖 1 中，我們顯示了優(yōu)化自動(dòng)代碼生成器的整體數(shù)據(jù)流，其中輸入模型稱為“用戶語(yǔ)言”，輸出稱為“源代碼”。多個(gè)階段被流水線化，原始模型中的第一階段讀數(shù)以用戶語(yǔ)言（M0）表示，并以某些內(nèi)部數(shù)據(jù)結(jié)構(gòu)（M1）表示模型。然后將其轉(zhuǎn)換為模型的較低級(jí)別表示（M2，M3等），直到最后階段以所需的編程語(yǔ)言生成實(shí)際的源代碼。要執(zhí)行集成測(cè)試，只需使用常規(guī)模型創(chuàng)建工具準(zhǔn)備一個(gè)以用戶語(yǔ)言表示的模型，將其饋送到代碼生成器中，然后檢查生成的源代碼，以確定它是否滿足形式和功能方面的高級(jí)要求，使用普通編譯器、靜態(tài)分析和該編程語(yǔ)言的測(cè)試工具。

相比之下，對(duì)多相代碼生成器的每個(gè)階段執(zhí)行單元測(cè)試要復(fù)雜得多。必須為給定階段的每個(gè)測(cè)試構(gòu)建一個(gè)內(nèi)部數(shù)據(jù)結(jié)構(gòu)，該結(jié)構(gòu)符合用于該階段輸入的表示形式，然后需要對(duì)該輸入調(diào)用該階段，然后必須檢查輸出表示以查看它是否具有預(yù)期的形式和內(nèi)容。準(zhǔn)備此類輸入并檢查此類輸出需要費(fèi)力的手動(dòng)過程或創(chuàng)建特殊工具，這些工具本身可能需要認(rèn)證。

集成單元測(cè)試

鑒于單元測(cè)試的復(fù)雜性，已經(jīng)開發(fā)了一種稱為集成單元測(cè)試的替代方法。圖 2 說(shuō)明了此方法：

［圖2 |集成單元測(cè)試方法是單元測(cè)試的更簡(jiǎn)單替代方法］

在圖 2 中，我們展示了一個(gè)將單元測(cè)試需求監(jiān)視器和單元測(cè)試預(yù)言機(jī)（一個(gè)“知道”所需輸出的檢查器）直接嵌入到工具結(jié)構(gòu)中的過程。將這些監(jiān)視器和檢查器嵌入到工具中后，我們按照用于正常集成測(cè)試的步驟進(jìn)行操作，準(zhǔn)備代表性模型（Test0 到 Test4），并通過代碼生成器將它們饋送。但是現(xiàn)在，每個(gè)嵌入式單元測(cè)試需求監(jiān)視器不只是等待工具生成最終輸出，而是跟蹤其關(guān)聯(lián)階段的輸入是否與其關(guān)聯(lián)的單元測(cè)試匹配，如果匹配，它會(huì)記錄該事實(shí)，然后觸發(fā)相應(yīng)的基于單元測(cè)試預(yù)言機(jī)的檢查器，該檢查器驗(yàn)證階段的輸出是否對(duì)應(yīng)于特定測(cè)試模式的輸入的預(yù)期轉(zhuǎn)換。

例如，假設(shè)我們?cè)谀Ｐ图?jí)別定義了增益塊的特定轉(zhuǎn)換，將其轉(zhuǎn)換為代碼級(jí)別的表達(dá)式，該表達(dá)式將信號(hào)變量的值乘以常量。每當(dāng)增益塊出現(xiàn)在其模型級(jí)輸入表示中時(shí)，我們都會(huì)有一個(gè)單元測(cè)試要求監(jiān)視器記錄，當(dāng)它出現(xiàn)時(shí)，觸發(fā)基于 oracle 的檢查器查看代碼級(jí)輸出表示，以確保它涉及將適當(dāng)?shù)男盘?hào)變量乘以適當(dāng)?shù)某?shù)。這是一個(gè)非常簡(jiǎn)單的檢查，只要有足夠的模型作為一個(gè)整體通過該工具，就可以預(yù)期覆蓋此特定的單元測(cè)試模式。

通過該工具運(yùn)行多個(gè)模型后，我們最終可以得到一個(gè)如圖 2 所示的表。在左側(cè)，我們有模型，Test0到Test4。在頂部，我們有針對(duì)工具每個(gè)不同階段的測(cè)試需求和測(cè)試預(yù)言機(jī)對(duì)。例如，tr0，2 表示階段 0 的測(cè)試要求 2，而 to2，1 表示階段 2 的測(cè)試預(yù)言機(jī) 1。每次階段的特定輸入滿足與某些測(cè)試需求相關(guān)的測(cè)試模式時(shí)，我們都會(huì)在輸入模型行的需求列中看到 SAT。每次調(diào)用測(cè)試預(yù)言機(jī)時(shí)，我們都會(huì)在輸入模型行的預(yù)言機(jī)列中看到 PASS 或 FAIL。如果我們最終得到一個(gè)空列，則從未遇到測(cè)試模式（未涵蓋相應(yīng)的低級(jí)要求）。如果我們最終在 test-oracle 列中出現(xiàn) FAIL，這意味著我們有一個(gè)測(cè)試失?。ㄏ鄳?yīng)的低級(jí)需求沒有正確實(shí)現(xiàn)）。在圖 2 所示的表中，我們看到 tr0，1 和 tr2，0 未被覆蓋，而 to0，2 和 to2，1 出現(xiàn)故障。這樣的表記錄了一個(gè)完整的單元測(cè)試過程，同時(shí)避免了為每個(gè)測(cè)試模式準(zhǔn)備特殊輸入的費(fèi)用。

值得信賴的代碼生成器

如果我們要越來(lái)越多地依賴此類工具來(lái)幫助從更高級(jí)別的模型自動(dòng)生成安全關(guān)鍵軟件，那么建立對(duì)代碼生成器的信任至關(guān)重要。但是，需要?jiǎng)?chuàng)新方法來(lái)管理在最高信任級(jí)別 TQL-1 下實(shí)現(xiàn)現(xiàn)代優(yōu)化代碼生成器的工具認(rèn)證的潛在高昂費(fèi)用。集成單元測(cè)試就是這樣一種方法。當(dāng)與其他用于正式指定需求并從這些需求生成需求監(jiān)視器和預(yù)言機(jī)等組件的系統(tǒng)方法結(jié)合使用時(shí)，可以實(shí)現(xiàn) TQL-1，這種方式不僅更具成本效益，而且隨著工具的發(fā)展支持增量鑒定。AdaCore 正在使用這些方法驗(yàn)證其 QGen 代碼生成器，從而為基于模型的開發(fā)社區(qū)提供一種新工具，該工具可以成為整體高完整性、軟件密集型系統(tǒng)工程流程的可信部分。

審核編輯：郭婷