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

01

引 言

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

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

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

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

02

核心技術(shù)

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

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

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

?通過(guò)可視化界面搭建設(shè)計(jì)模型：設(shè)計(jì)模型的構(gòu)建通常基于圖形化組件，這些組件可以是節(jié)點(diǎn)、邊、狀態(tài)機(jī)狀態(tài)等。每個(gè)組件都有明確的語(yǔ)義，例如節(jié)點(diǎn)表示一個(gè)功能模塊，邊表示數(shù)據(jù)流或控制流?？梢暬缑嬷С滞戏挪僮?，用戶可以通過(guò)拖動(dòng)組件并將其放置在設(shè)計(jì)區(qū)域來(lái)構(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語(yǔ)言的轉(zhuǎn)化：設(shè)計(jì)模型中的每個(gè)節(jié)點(diǎn)需要映射為L(zhǎng)ustre語(yǔ)言中的一個(gè)節(jié)點(diǎn)（Node）。節(jié)點(diǎn)的輸入輸出信號(hào)需要與設(shè)計(jì)模型中的接口一致。設(shè)計(jì)模型中的數(shù)據(jù)流邊需要轉(zhuǎn)化為L(zhǎng)ustre語(yǔ)言中的數(shù)據(jù)連接。每個(gè)邊的源節(jié)點(diǎn)輸入需要連接到目標(biāo)構(gòu)件的輸出。設(shè)計(jì)模型中的控制流邏輯（如分支和循環(huán)）需要轉(zhuǎn)化為L(zhǎng)ustre語(yǔ)言中的條件語(yǔ)句和迭代器結(jié)構(gòu)。

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

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

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

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

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

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

03

實(shí)例解析

本章節(jié)通過(guò)真實(shí)世界中的飛機(jī)機(jī)翼轉(zhuǎn)向控制系統(tǒng)中的一個(gè)警告子模塊實(shí)例對(duì)基于模型的測(cè)試用例生成進(jìn)行詳細(xì)說(shuō)明。該警告子模塊的需求為，輸入左右機(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)過(guò)Flatten構(gòu)件（拆分結(jié)構(gòu)體構(gòu)件）裂化為兩個(gè)浮點(diǎn)數(shù)分別與rollRate進(jìn)行大小比較，將比較結(jié)果作為輸出返回。

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

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

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

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

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

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

?符號(hào)化輸入：將輸入 rollRate 符號(hào)化為符號(hào)變量 rollRate_sym。

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

leftWarning 的路徑條件：rollRate_sym < _L15

rightWarning 的路徑條件：rollRate_sym > _L16

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

rollRate_sym < -15.0與rollRate_sym >15

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

對(duì)于 leftWarning 為 true 的情況：rollRate_sym < -15.0

對(duì)于 leftWarning 為 false 的情況：rollRate_sym >= -15.0

對(duì)于 rightWarning 為 true 的情況：rollRate_sym > 15.0

對(duì)于 rightWarning 為 false 的情況：rollRate_sym <= 15.0

?測(cè)試用例生成：通過(guò)對(duì)上述約束組合后作為約束求解器Z3的輸入以進(jìn)行求解，能夠得到以下最簡(jiǎn)測(cè)試用例集。

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

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

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

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

04

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

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

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

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

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

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

05

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

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

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

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

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

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

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

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

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

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

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

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

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

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

審核編輯 黃宇