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

01

引 言

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

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

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

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

02

核心技術(shù)

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

（一）設(shè)計(jì)模型構(gòu)建和解析

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

?通過可視化界面搭建設(shè)計(jì)模型：設(shè)計(jì)模型的構(gòu)建通?；趫D形化組件，這些組件可以是節(jié)點(diǎn)、邊、狀態(tài)機(jī)狀態(tài)等。每個(gè)組件都有明確的語義，例如節(jié)點(diǎn)表示一個(gè)功能模塊，邊表示數(shù)據(jù)流或控制流。可視化界面支持拖放操作，用戶可以通過拖動(dòng)組件并將其放置在設(shè)計(jì)區(qū)域來構(gòu)建模型。這種直觀的操作方式大大降低了模型構(gòu)建的難度。支持層次化結(jié)構(gòu)的構(gòu)建，用戶可以將復(fù)雜的系統(tǒng)分解為多個(gè)子系統(tǒng)，并在不同的層次上進(jìn)行建模。這種層次化結(jié)構(gòu)不僅有助于理解系統(tǒng)的整體結(jié)構(gòu)，還能提高模型的可維護(hù)性。

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

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

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

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

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

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

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

03

實(shí)例解析

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

（一）設(shè)計(jì)模型構(gòu)建

根據(jù)需求進(jìn)行設(shè)計(jì)模型的構(gòu)建，其可視化模型如下所示。

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

該模型包含一個(gè)輸入與兩個(gè)輸出。輸入為rollRate，表示當(dāng)前飛機(jī)的預(yù)期的轉(zhuǎn)向率，輸出分別為左機(jī)翼與右機(jī)翼的警告情況。在可視化模型的最左側(cè)為常量kRollRateWarning，其類型為結(jié)構(gòu)體，結(jié)構(gòu)體包含兩個(gè)浮點(diǎn)數(shù)。常量kRollRateWarning經(jīng)過Flatten構(gòu)件（拆分結(jié)構(gòu)體構(gòu)件）裂化為兩個(gè)浮點(diǎn)數(shù)分別與rollRate進(jìn)行大小比較，將比較結(jié)果作為輸出返回。

將該設(shè)計(jì)模型轉(zhuǎn)換為Lustre語言代碼，并確保其能通過檢查。其Lustre語言代碼如下所示。

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

最后進(jìn)行中間模型轉(zhuǎn)換，以將Lustre模型轉(zhuǎn)換為可直接操縱的C++語言模型。通過對輸入的Lustre語言模型進(jìn)行分析，生成相應(yīng)的抽象語法樹。繼而通過對生成的抽象數(shù)據(jù)字典的管理，來實(shí)現(xiàn)中間模型中定義的數(shù)據(jù)變量關(guān)系的轉(zhuǎn)換與存儲(chǔ)。最終，作為輸入的Lustre語言模型將轉(zhuǎn)化為具有結(jié)構(gòu)化與層次化信息，且便于操作的C++語言中間模型。

圖3 中間模型轉(zhuǎn)換流程圖

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

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

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

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

leftWarning 的路徑條件：rollRate_sym < _L15

rightWarning 的路徑條件：rollRate_sym > _L16

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

rollRate_sym < -15.0與rollRate_sym >15

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

對于 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的輸入以進(jìn)行求解，能夠得到以下最簡測試用例集。

測試用例 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 函數(shù) RollRateWarning 進(jìn)行全面的測試。符號執(zhí)行不僅能夠生成覆蓋所有路徑的測試用例，還能發(fā)現(xiàn)潛在的邊界條件和異常情況。結(jié)合 Lustre 語言的特性，符號執(zhí)行為實(shí)時(shí)嵌入式系統(tǒng)的測試提供了一種高效、可靠的方法。

04

優(yōu)勢總結(jié)

在軟件開發(fā)領(lǐng)域，測試用例生成是確保軟件質(zhì)量的關(guān)鍵環(huán)節(jié)。基于模型的測試用例生成作為一種先進(jìn)的測試方法，相較于傳統(tǒng)測試用例生成方法，具有多方面的顯著優(yōu)勢。

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

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

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

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

05

技術(shù)應(yīng)用

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

圖4 SmartRocket Modeler項(xiàng)目管理界面圖

依托模型驅(qū)動(dòng)測試用例生成技術(shù)，上海控安 SmartRocket Modeler 團(tuán)隊(duì)通過深入調(diào)研與持續(xù)實(shí)踐，實(shí)現(xiàn)了從理論到應(yīng)用的有效轉(zhuǎn)化。

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

圖5 SmartRocket Modeler設(shè)計(jì)模型圖形化展示界面

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

圖6 RollControl飛機(jī)控制RollRateWarning模塊Lustre代碼示意圖

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

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

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

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

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

圖9 測試用例生成結(jié)果

審核編輯 黃宇