在當今復雜多變的軟件開發(fā)環(huán)境中，軟件系統(tǒng)的規(guī)模和復雜度不斷攀升，傳統(tǒng)測試方法面臨著諸多挑戰(zhàn)。如何高效、準確地生成測試用例，以確保軟件系統(tǒng)的質量和可靠性，成為軟件測試領域的關鍵問題之一。而基于模型的測試用例生成（Model-Based Test Case Generation）作為一種新興且高效的測試方法，正逐漸成為解決這一問題的重要手段。

01

引 言

在傳統(tǒng)的軟件測試過程中，測試用例多由人工基于源代碼撰寫，往往依賴于開發(fā)人員或測試工程師對需求與代碼的經驗和直覺。這種方法雖然在一定程度上能夠發(fā)現一些明顯的缺陷，但隨著軟件系統(tǒng)的復雜度增加，其局限性愈發(fā)明顯。開發(fā)人員很難全面覆蓋所有的測試場景，尤其是那些隱藏在復雜邏輯和交互中的潛在問題。此外，傳統(tǒng)測試用例生成方法的效率較低，難以滿足快速迭代和頻繁更新的軟件開發(fā)需求。

基于模型的測試用例生成（Model-Based Test Case Generation）應運而生，它通過構建軟件系統(tǒng)的模型，將測試用例的生成從繁瑣的人工設計轉變?yōu)榛谀Ｐ偷淖詣踊^程。這種方法不僅能夠提高測試用例的質量和覆蓋率，還能顯著提升測試效率，減少測試成本，將開發(fā)人員與測試人員從復雜的需求與代碼中解放出來。

在基于模型的測試中，軟件系統(tǒng)的設計模型是核心。它以具體的模型描述系統(tǒng)的結構、行為和約束條件，通過對設計模型的構建、分析和遍歷，利用符號執(zhí)行方法與SMT求解器（Satisfiability Modulo Theories Solver）自動生成測試用例，覆蓋系統(tǒng)的關鍵功能和潛在故障點。這種方法的優(yōu)勢在于，它能夠從系統(tǒng)的整體視角出發(fā)，考慮各種可能的交互和狀態(tài)轉換，從而生成更為全面和有效的測試用例。

在接下來的內容中，我們將深入探討基于模型的測試用例生成，并結合Lustre這一獨特的同步數據流語言，展示符號執(zhí)行在基于模型的測試用例執(zhí)行中的應用和優(yōu)勢。通過實際案例和分析，揭示基于模型的測試用例生成方法如何幫助開發(fā)人員和測試工程師更高效地發(fā)現軟件缺陷，提升軟件質量。

02

核心技術

基于模型的測試用例生成主要包含兩個核心技術，分別是設計模型構建和解析與符號執(zhí)行生成用例。

（一）設計模型構建和解析

在基于模型的測試中，設計模型是測試用例生成的基礎。設計模型的構建通常需要一個直觀且易于操作的界面，以便開發(fā)人員和測試人員能夠根據需求快速搭建出系統(tǒng)的模型。而對于Lustre語言，設計模型的構建和解析尤為重要，因為Lustre的同步數據流特性需要精確地描述系統(tǒng)的時序行為。其主要流程如下：

?通過可視化界面搭建設計模型：設計模型的構建通常基于圖形化組件，這些組件可以是節(jié)點、邊、狀態(tài)機狀態(tài)等。每個組件都有明確的語義，例如節(jié)點表示一個功能模塊，邊表示數據流或控制流?？梢暬缑嬷С滞戏挪僮鳎脩艨梢酝ㄟ^拖動組件并將其放置在設計區(qū)域來構建模型。這種直觀的操作方式大大降低了模型構建的難度。支持層次化結構的構建，用戶可以將復雜的系統(tǒng)分解為多個子系統(tǒng)，并在不同的層次上進行建模。這種層次化結構不僅有助于理解系統(tǒng)的整體結構，還能提高模型的可維護性。

?可視化模型到Lustre語言的轉化：設計模型中的每個節(jié)點需要映射為Lustre語言中的一個節(jié)點（Node）。節(jié)點的輸入輸出信號需要與設計模型中的接口一致。設計模型中的數據流邊需要轉化為Lustre語言中的數據連接。每個邊的源節(jié)點輸入需要連接到目標構件的輸出。設計模型中的控制流邏輯（如分支和循環(huán)）需要轉化為Lustre語言中的條件語句和迭代器結構。

?中間模型的生成：使用Lustre編譯器或解析器工具，將Lustre程序解析為抽象語法樹（AST）。解析過程需要確保語法和語義的正確性。從AST中提取數據流圖，包括節(jié)點、邊和信號類型。數據流圖的每個節(jié)點對應Lustre程序中的一個節(jié)點，每條邊對應一個等式連接，所有的節(jié)點與等式都轉化為可供操作的C++語言對象或實例。完成中間模型的轉化后還要對其進行靜態(tài)檢查，以保證模型的正確性與一致性。

（二）符號執(zhí)行生成用例

符號執(zhí)行是一種動態(tài)分析技術，它通過分析輸入的中間模型（C++語言實例），符號化輸入和路徑條件，探索程序的所有可能執(zhí)行路徑。符號執(zhí)行的核心思想是將程序的輸入表示為符號變量，而不是具體的數值。這些符號變量在程序的執(zhí)行過程中被逐步約束，最終通過求解約束條件生成具體的測試用例。

?符號變量與路徑條件：在符號執(zhí)行中，程序的輸入被表示為符號變量。 這些符號變量可以是整數、浮點數或布爾值等。符號變量在程序的執(zhí)行過程中被逐步約束。路徑條件是符號執(zhí)行中用于描述程序執(zhí)行路徑的邏輯表達式。每個路徑條件表示從程序入口到當前節(jié)點的路徑上所有分支條件的合取。路徑條件的求解結果決定了程序的執(zhí)行路徑。

?約束求解：在符號執(zhí)行過程中，程序的每一條路徑都被表示為一組約束條件。這些約束條件是路徑條件的集合，描述了程序在該路徑上的輸入輸出關系。符號執(zhí)行需要一個強大的約束求解器來求解生成的約束條件。常見的約束求解器包括Z3、CVC5等。這些求解器能夠處理線性方程、非線性方程、布爾邏輯等多種約束條件。

?測試用例生成：符號執(zhí)行通過逐步探索程序的所有可能路徑，生成路徑條件。對于每個路徑條件，約束求解器嘗試找到滿足條件的輸入值。如果約束求解器能夠找到滿足路徑條件的輸入值，則這些輸入值被用作測試用例。符號執(zhí)行的目標是生成覆蓋程序所有路徑的測試用例。

03

實例解析

本章節(jié)通過真實世界中的飛機機翼轉向控制系統(tǒng)中的一個警告子模塊實例對基于模型的測試用例生成進行詳細說明。該警告子模塊的需求為，輸入左右機翼的轉向率，與預先設定的常數分別進行比較，并將結果返回。

（一）設計模型構建

根據需求進行設計模型的構建，其可視化模型如下所示。

圖1 機翼轉向控制系統(tǒng)警告子模塊可視化模型

該模型包含一個輸入與兩個輸出。輸入為rollRate，表示當前飛機的預期的轉向率，輸出分別為左機翼與右機翼的警告情況。在可視化模型的最左側為常量kRollRateWarning，其類型為結構體，結構體包含兩個浮點數。常量kRollRateWarning經過Flatten構件（拆分結構體構件）裂化為兩個浮點數分別與rollRate進行大小比較，將比較結果作為輸出返回。

將該設計模型轉換為Lustre語言代碼，并確保其能通過檢查。其Lustre語言代碼如下所示。

圖2 機翼轉向控制系統(tǒng)警告子模塊Lustre模型

最后進行中間模型轉換，以將Lustre模型轉換為可直接操縱的C++語言模型。通過對輸入的Lustre語言模型進行分析，生成相應的抽象語法樹。繼而通過對生成的抽象數據字典的管理，來實現中間模型中定義的數據變量關系的轉換與存儲。最終，作為輸入的Lustre語言模型將轉化為具有結構化與層次化信息，且便于操作的C++語言中間模型。

圖3 中間模型轉換流程圖

（二）符號執(zhí)行生成用例

對給定的 Lustre 函數 RollRateWarning 使用符號執(zhí)行方法，包括符號執(zhí)行過程、約束條件生成與求解、測試用例生成等關鍵步驟。

?符號化輸入：將輸入 rollRate 符號化為符號變量 rollRate_sym。

?路徑條件生成：根據函數邏輯，我們可以得到以下路徑條件：

leftWarning 的路徑條件：rollRate_sym < _L15

rightWarning 的路徑條件：rollRate_sym > _L16

由于_L15與_L16是由常數kRollRateWarning裂化而來，在當前場景下kRollRateWarning被設定為(-15.0,15.0)。因此路徑條件實際上分別為：

rollRate_sym < -15.0與rollRate_sym >15

?約束求解：需要求解以下約束條件，以生成符合航空航天軟件中廣泛使用的MC/DC覆蓋率準則下的測試用例。

對于 leftWarning 為 true 的情況：rollRate_sym < -15.0

對于 leftWarning 為 false 的情況：rollRate_sym >= -15.0

對于 rightWarning 為 true 的情況：rollRate_sym > 15.0

對于 rightWarning 為 false 的情況：rollRate_sym <= 15.0

?測試用例生成：通過對上述約束組合后作為約束求解器Z3的輸入以進行求解，能夠得到以下最簡測試用例集。

測試用例 1：rollRate = -16.0（滿足 leftWarning = true 和 rightWarning = false）

測試用例 2：rollRate = -15.0（滿足 leftWarning = false 和 rightWarning = false）

測試用例 3：rollRate =16（滿足 leftWarning = false 和 rightWarning = true）

通過符號執(zhí)行方法，我們可以對 Lustre 函數 RollRateWarning 進行全面的測試。符號執(zhí)行不僅能夠生成覆蓋所有路徑的測試用例，還能發(fā)現潛在的邊界條件和異常情況。結合 Lustre 語言的特性，符號執(zhí)行為實時嵌入式系統(tǒng)的測試提供了一種高效、可靠的方法。

04

優(yōu)勢總結

在軟件開發(fā)領域，測試用例生成是確保軟件質量的關鍵環(huán)節(jié)?；谀Ｐ偷臏y試用例生成作為一種先進的測試方法，相較于傳統(tǒng)測試用例生成方法，具有多方面的顯著優(yōu)勢。

(一) 提高測試覆蓋率：通過構建軟件系統(tǒng)的模型，能夠全面覆蓋系統(tǒng)的各種行為和狀態(tài)轉換。模型可以精確地描述系統(tǒng)的功能、業(yè)務流程以及輸入輸出之間的關系，確保測試用例能夠覆蓋所有關鍵路徑和邊界條件。

(二) 提升測試效率：能夠自動化地從模型中生成測試用例，大大減少了人工編寫測試用例的時間和精力。測試人員只需專注于模型的構建和維護，而無需花費大量時間在測試用例的編寫上。當軟件需求發(fā)生變更時，只需更新模型，方法就可以快速重新生成測試用例，以適應新的需求。這種快速響應能力使得該方法在敏捷開發(fā)和持續(xù)集成環(huán)境中具有顯著優(yōu)勢。

(三) 增強測試可維護性：測試用例是基于模型生成的，因此測試用例的維護可以轉化為對模型的維護。模型的修改和維護相對簡單，且更容易保持一致性。當模型更新時，所有相關的測試用例可以同步更新，避免了傳統(tǒng)測試中測試用例分散、難以維護的問題。

(四) 提升測試質量：由于測試用例是基于模型自動生成的，因此可以減少因人工編寫測試用例而引入的錯誤。自動生成的測試用例更加客觀、準確，能夠更有效地發(fā)現軟件缺陷。生成的測試用例具有高度的一致性和可重復性。在相同的模型和生成規(guī)則下，每次生成的測試用例都是相同的，這有助于測試結果的比較和分析。

05

技術應用

隨著科技發(fā)展與技術創(chuàng)新，近年來軌交、汽車、航空航天等領域的發(fā)展非常迅猛，伴隨而來的是各類安全問題。以上領域涉及的安全關鍵軟件的質量與效率都受到了高度重視。因此，可視化建模工具SmartRocket Modeler應運而生，誕生自質量，扎根于安全。通過模型語言的圖形化建模、模型靜態(tài)檢查、仿真與調試以及C代碼生成等等功能為用戶提供一套基于模型的高安全性嵌入式軟件解決方案。在更進一步的前提下逐漸替代相關國外軟件，為解決卡脖子難題做出貢獻。

圖4 SmartRocket Modeler項目管理界面圖

依托模型驅動測試用例生成技術，上?？匕?SmartRocket Modeler 團隊通過深入調研與持續(xù)實踐，實現了從理論到應用的有效轉化。

Modeler的輸入為需求模型，通過工程師的建?；驅肷煞椒ǖ玫狡湓O計模型，其設計模型能夠通過圖形化或者代碼字符串的方式進行展示，如下圖所示為Modeler官方示例項目Roll Control的圖形化界面。

圖5 SmartRocket Modeler設計模型圖形化展示界面

Modeler使用同步數據流語言Lustre代碼進行設計模型的一致性描述，Lustre是一種經過嚴格形式化驗證的設計模型語言，它能夠充分描述機載軟件在固定時鐘下的運行情況，其示例代碼如下所示。

圖6 RollControl飛機控制RollRateWarning模塊Lustre代碼示意圖

Modeler通過本文的完整方法與理論，針對設計模型自動生成滿足MC/DC覆蓋率的準則的測試用例。點擊圖形界面中的“生成用例”按鈕，工具會根據當前模型節(jié)點信息生成用例。

圖7 圖形界面“生成用例”按鈕

用例生成完畢后，工具會將所有用例集成到Excel表格中，并提供管理與查看功能。

圖8 圖形界面用例下載管理器

針對該模型節(jié)點，即機翼轉向控制系統(tǒng)警告子模塊，得出的全部測試用例如下。

圖9 測試用例生成結果

審核編輯 黃宇