您如何建立對用于安全關(guān)鍵系統(tǒng)的自動代碼生成器的信任？例如，給定一個代碼生成器，它采用 Simulink 和 Stateflow 中表示的飛行控制系統(tǒng)的實時模型并將其轉(zhuǎn)換為 MISRA C 或 Ada 的 SPARK 子集，什么過程可以確保生成的代碼是真實的表示原來的實時模型？美國聯(lián)邦航空管理局 （FAA） 有一個定義明確的過程來創(chuàng)建合格的代碼生成器，這意味著代碼生成器的輸出可以被信任以與輸入模型的語義完全匹配，沒有遺漏，也沒有添加任何內(nèi)容。此過程在 DO-178C（機(jī)載系統(tǒng)中的軟件考慮）中定義，

對于像代碼生成器這樣的工具，它可能會在機(jī)載系統(tǒng)中插入錯誤，如果該工具要用于其故障可能發(fā)生的子系統(tǒng)，則需要最高級別的工具認(rèn)證（工具認(rèn)證級別 1 （TQL-1））是災(zāi)難性的（A 級子系統(tǒng)）。

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

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

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

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

從高級需求中導(dǎo)出模塊級需求，這些需求足夠具體以確定適當(dāng)?shù)膶崿F(xiàn)

使用單元測試檢查實現(xiàn)的每個模塊是否符合其低級需求

對所有高級需求執(zhí)行集成級測試

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

對于嵌入式軟件組件，每個模塊的單元級測試和整個組件的集成級測試的組合可以很好地工作。特別是嵌入式軟件模塊的單元測試是實用的，因為在許多情況下，每個模塊的輸入的數(shù)量和復(fù)雜性是可控的，并且輸出相對容易識別和檢查。然而，對于像自動代碼生成器這樣的工具，它通常涉及多個階段，涉及將輸入模型逐步轉(zhuǎn)換為生成的代碼，單元測試可能是一個真正的挑戰(zhàn)。另一方面，對于這樣的工具，集成測試并不難，因為中間階段的數(shù)量不會影響工具的整體輸入和輸出。

圖 1 說明了單元測試的復(fù)雜性和代碼生成器等多階段工具的集成測試相對容易性之間的這種二分法。

【圖1 | 由于易于使用，集成測試優(yōu)于單元測試。］

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

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

集成單元測試

考慮到單元測試的復(fù)雜性，已經(jīng)開發(fā)了一種替代方法，稱為集成單元測試。圖 2 說明了這種方法：

【圖2 | 集成單元測試方法是單元測試的一種更簡單的替代方法］

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

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

通過該工具運行多個模型后，我們可以得到一個類似于圖 2 的表格。在左側(cè)，我們有模型，從 Test 0到 Test 4。在頂部，我們有工具每個不同階段的測試需求和測試預(yù)言對。例如，tr 0，2表示階段 0 的測試要求 2，而2，1表示階段 2 的測試預(yù)言 1。每當(dāng)一個階段的特定輸入滿足與某個測試需求關(guān)聯(lián)的測試模式時，我們將在輸入模型行的需求列中看到一個 SAT。每次調(diào)用測試 oracle 時，我們都會在輸入模型行的 oracle 列中看到 PASS 或 FAIL。如果我們最終得到一個空列，則永遠(yuǎn)不會遇到測試模式（未涵蓋相應(yīng)的低級需求）。如果我們最終在 test-oracle 列中出現(xiàn) FAIL，這意味著我們有一個測試失敗（相應(yīng)的低級需求沒有正確實現(xiàn)）。在圖 2 所示的表格中，我們看到 tr 0，1和 tr 2，0沒有被覆蓋，而 to 0，2和 to 2，1有失敗。這樣的表格記錄了完整的單元測試過程，同時避免了為每個測試模式準(zhǔn)備特殊輸入的費用。

受信任的代碼生成器

如果我們要越來越依賴此類工具來幫助從更高級別的模型自動生成安全關(guān)鍵軟件，那么建立對代碼生成器的信任至關(guān)重要。但是，需要創(chuàng)新方法來管理以最高信任級別 TQL-1 實現(xiàn)現(xiàn)代優(yōu)化代碼生成器的工具認(rèn)證的潛在高昂費用。集成單元測試就是這樣一種方法。當(dāng)與其他正式指定需求的系統(tǒng)方法相結(jié)合，并根據(jù)這些需求生成需求監(jiān)控器和預(yù)言機(jī)等組件時，就有可能以一種不僅更具成本效益，而且支持增量認(rèn)證的方式實現(xiàn) TQL-1。工具進(jìn)化。AdaCore 正在使用這些方法驗證其 QGen 代碼生成器。

審核編輯：郭婷