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

對于像代碼生成器這樣的工具，可能會將錯誤插入機載系統，如果要將工具用于故障可能是災難性的子系統（A 級子系統），則需要最高級別的工具資格（工具資格級別 1 （TQL-1））。

毫不奇怪，這種級別的工具鑒定可能涉及大量的時間和精力，通常估計為每 1，000 行代碼 （KSLOC） 數百小時。這類似于驗證 A 級安全關鍵型嵌入式軟件組件所需的每行工作量。但是工具可以有更多的代碼行。例如，如果該工具是100 KSLOC，則傳統的A級驗證方法可能花費約500萬美元。因此，有強烈的動機研究測試此類工具的替代方法，同時仍然實現TQL-1目標。

傳統的測試方法

驗證高完整性應用程序的傳統方法要求測試人員：

仔細定義和驗證應用程序的一組高級要求

從高級需求派生模塊級需求，這些要求足夠具體，可以確定適當的實現

使用單元測試根據其低級需求檢查實現的每個模塊

對所有高級需求執行集成級測試

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

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

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

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

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

相比之下，對多相代碼生成器的每個階段執行單元測試要復雜得多。必須為給定階段的每個測試構建一個內部數據結構，該結構符合用于該階段輸入的表示形式，然后需要對該輸入調用該階段，然后必須檢查輸出表示以查看它是否具有預期的形式和內容。準備此類輸入并檢查此類輸出需要費力的手動過程或創建特殊工具，這些工具本身可能需要認證。

集成單元測試

鑒于單元測試的復雜性，已經開發了一種稱為集成單元測試的替代方法。圖 2 說明了此方法：

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

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

例如，假設我們在模型級別定義了增益塊的特定轉換，將其轉換為代碼級別的表達式，該表達式將信號變量的值乘以常量。每當增益塊出現在其模型級輸入表示中時，我們都會有一個單元測試要求監視器記錄，當它出現時，觸發基于 oracle 的檢查器查看代碼級輸出表示，以確保它涉及將適當的信號變量乘以適當的常數。這是一個非常簡單的檢查，只要有足夠的模型作為一個整體通過該工具，就可以預期覆蓋此特定的單元測試模式。

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

值得信賴的代碼生成器

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

審核編輯：郭婷