基于SPIN的功能測試用例生成方法研究

李建 楊晉吉

摘要摘要：提出了一種自動生成系統(tǒng)功能測試用例的新方法。該方法使用Promela語言對軟件系統(tǒng)的狀態(tài)和行為進(jìn)行描述建模，使用LTL公式描述測試覆蓋標(biāo)準(zhǔn)，然后將該組LTL公式和描述狀態(tài)行為的Promela模型輸入SPIN模型檢測工具，并利用模型檢測工具自動生成相應(yīng)的證據(jù)路徑，最后結(jié)合正例將路徑轉(zhuǎn)化成滿足相應(yīng)覆蓋標(biāo)準(zhǔn)的系統(tǒng)功能測試用例，并以電梯系統(tǒng)模型對該方法作出了詮釋。

關(guān)鍵詞關(guān)鍵詞：功能測試用例；SPIN；模型檢測；Promela建模

DOIDOI：10.11907/rjdk.161463

中圖分類號：TP306文獻(xiàn)標(biāo)識碼：A文章編號文章編號：16727800（2016）007000103

0引言

軟件測試是指新開發(fā)出來的軟件運(yùn)用于實際生產(chǎn)前，對其需求的分析、設(shè)計規(guī)格的說明以及最終編碼的復(fù)核審查，它是保證軟件質(zhì)量的關(guān)鍵步驟。利用最少的時間和測試用例來找到軟件開發(fā)過程中各階段潛在的錯誤以保證該開發(fā)軟件的質(zhì)量，是軟件測試的最終目的和終極目標(biāo)。

為改變近年來人們對軟件測試用例生成全靠手工完成的狀況，同時滿足自動化生成測試用例的需求，本文提出一種基于SPIN工具的系統(tǒng)功能測試用例自動化生成方法。首先，將待測系統(tǒng)的行為及狀態(tài)基于符號的執(zhí)行從源代碼中抽取出來；然后，使用一組線性時態(tài)邏輯（LTL）公式描述特定的覆蓋標(biāo)準(zhǔn)；最后，將建立好的Promela模型與代表系統(tǒng)屬性的LTL公式一起輸入到SPIN中進(jìn)行檢測。如此，就將模型檢測工具的自動化驗證過程轉(zhuǎn)化成了測試用例生成過程，即SPIN生成的與LTL公式相對應(yīng)的證據(jù)路徑。圖1為基于SPIN的自動生成測試用例技術(shù)框架。

1基于SPIN的測試用例生成基本思路

SPIN是由美國貝爾實驗室開發(fā)出來的模型檢測器，它主要用來對非實時系統(tǒng)模型進(jìn)行檢測，即驗證某個有窮狀態(tài)的系統(tǒng)是否滿足利用LTL公式描述的屬性。本文將系統(tǒng)功能測試用例生成的問題轉(zhuǎn)化為一個模型檢測問題，將生成測試用例的問題變換成驗證模型檢測中“狀態(tài)不可達(dá)”、“不存在此條路徑”等性質(zhì)的問題。通過建立SUT行為模型，將一個測試覆蓋標(biāo)準(zhǔn)構(gòu)建為模型檢測器的驗證條件，并將模型檢測得到的反例變換成測試用例集。由于模型檢測工具能夠利用生成的反例來解釋違反了應(yīng)滿足系統(tǒng)性質(zhì)的情況，因而此種反例很適合作為功能測試的路徑。

為了利用模型檢測過程得到的反例來生成測試用例集，需要取反用時序邏輯公式描述的測試覆蓋標(biāo)準(zhǔn)，即假設(shè)測試覆蓋標(biāo)準(zhǔn)永不為真，對原有的時序邏輯描述特性進(jìn)行否定。檢測時，若檢測到系統(tǒng)與某個時序邏輯描述不一致，就會生成反例，說明模型不滿足性質(zhì)的原因，這是可能的一個測試用例的序列。當(dāng)反復(fù)驗證所有性質(zhì)時，可以得到一系列能實現(xiàn)測試覆蓋標(biāo)準(zhǔn)的測試用例的序列。2系統(tǒng)建模與模型檢測

采用模型檢測技術(shù)對被測系統(tǒng)和測試覆蓋標(biāo)準(zhǔn)進(jìn)行形式化描述，本文采用Promela描述被測系統(tǒng)，用 LTL 描述測試覆蓋標(biāo)準(zhǔn)。2.1Promela建模

不是一般的程序語言，而是一款專用來描述并發(fā)系統(tǒng)的模型語言，用來建模有限狀態(tài)系統(tǒng)。它類似于C語言的語法結(jié)構(gòu)，能夠動態(tài)地創(chuàng)建并行進(jìn)程，進(jìn)程間的通訊通過消息通道來實現(xiàn)，通訊方式有2種：異步、同步。由Promela建立的模型組成包括進(jìn)程、消息通道、對象和變量等，如圖3所示。

2.2LTL公式邏輯描述

與CTL相比較，LTL更適合對并發(fā)程序的性質(zhì)進(jìn)行驗證，所以本文使用的是LTL邏輯公式。在SPIN中，LTL算子包含有&&、||、→、！和3種時序算子：① <> p：表示p在未來的某個狀態(tài)點成立；② p：表示p在未來的所有狀態(tài)點都成立；③ p∪q：表示p在所有狀態(tài)點都成立直到遇到第一個狀態(tài)點使q成立。在iSpin中，必須對每一個用到的LTL符號增加一個宏定義，即聲明p、q所代表的等式。 2.3SPIN檢測

SPIN由貝爾實驗室用ANSI C開發(fā)，可在所有UNIX操作系統(tǒng)版本中使用，也可在安裝了Windows 95以上版本、Linux等操作系統(tǒng)中使用。 SPIN工具的思想是求兩個自動機(jī)的交集，如果為空集，則安全特性得到驗證，否則輸出不滿足該安全特性的行為軌跡。

采用形式化公式來表達(dá)，即證明M╞是否成立，其中，M表示模型，表示時態(tài)邏輯公式。分別將轉(zhuǎn)換成自動機(jī)A，將M轉(zhuǎn)換成AM，即相當(dāng)于證明：

2.4反例分析

SPIN采用雙重深度優(yōu)先搜索方式進(jìn)行狀態(tài)搜索，遇到反例路徑后就退出搜索，并將路徑打印到一個后綴名為“.trail”的文件里。這種方法的優(yōu)點是完全自動化，系統(tǒng)若不滿足給定的性質(zhì)，檢驗結(jié)果就給出反例，生成的反例反映一個狀態(tài)變換的路徑，該路徑包括一序列步驟，相應(yīng)狀態(tài)的取值在每一步驟中都會被給出?？梢杂孟到y(tǒng)簡化的模型來反例跟蹤，再結(jié)合正例來比較就可總結(jié)得出所需要的系統(tǒng)功能測試用例。3實驗驗證

3.1電梯系統(tǒng)

電梯在運(yùn)行時分為如下3種狀態(tài)：①空閑狀態(tài)：電梯沒有發(fā)出目的層呼叫信號和呼叫電梯信號；②等待狀態(tài)：開始響應(yīng)某一個呼叫電梯的信號，或有乘客正進(jìn)、出電梯；③運(yùn)行狀態(tài)：正在響應(yīng)某一個呼叫電梯信號。電梯系統(tǒng)運(yùn)行模型如圖5所示。

3.2建模與LTL

3.2.1模型的Promela描述

為了舉例描述本文提出的方法，本次建模只是選取了1個人、上下4層樓電梯的模型作為例子，涉及3個進(jìn)程Person（）、Servis（）、Elevator（）以及3個通道：

3.2.2LTL性質(zhì)描述

以下性質(zhì)以乘客去3樓為例，建立檢驗規(guī)約，去其它樓層同理可行。

（（going_to==3）-><>（at_floor==3）），此條性質(zhì)說明乘客將要去3樓，則在以后的運(yùn)行狀態(tài)中該電梯必須有一個狀態(tài)為到達(dá)并停在3樓的情況。

（（going_to==3）-><>?。╝t_floor==3）），此性質(zhì)為實驗的缺陷性質(zhì)，即將原本成立的性質(zhì)全部或部分取反，如果驗證工具給出反例，則說明該性質(zhì)是不滿足的。從反例給出的路徑可以分析得到想要的功能測試用例。

3.2.3驗證與結(jié)果

首先在官網(wǎng)下載cygwin軟件（用于虛擬Linux環(huán)境），點擊下載安裝所有安裝包，以免出錯；然后啟動XWin server服務(wù)器（用于生成iSpin界面）；最后啟用iSpin，導(dǎo)入已完成系統(tǒng)建模的Promela描述。

進(jìn)行語法檢驗，Syntax Check，得到結(jié)果顯示無語法錯誤，并且提示有用到2個ltl公式分別為e1、e2。

點擊Verification，選擇use claim，驗證性質(zhì)e1，點擊run。從結(jié)果可看到State-vector 68 byte， depth reached 1162， errors：0，還可以在最后一行看到No errors found -- did you verify all claims？由此可知e1性質(zhì)滿足該系統(tǒng)正常運(yùn)行。

同理，可以驗證e2。從e2的結(jié)果圖中可看到State-vector 68 byte， depth reached 164， errors：1，可知該性質(zhì)不支持該驗證系統(tǒng)的正常運(yùn)行，并且由最后一行提示：To replay the error-trail， goto Simulate/Replay and select“run”可知已經(jīng)自動生成了反例。最后可以切換到Simulate/Replay 選擇Guided，with trail：Elevator_protocol.pml.trail browse 點擊“（Re）Run”，得到反例結(jié)果路徑。

由e2這一陷阱性質(zhì)可以知，該性質(zhì)是不滿足該電梯系統(tǒng)的，即說明存在乘客將要去3樓，則在以后的運(yùn)行狀態(tài)中該電梯必須有一個狀態(tài)為到達(dá)并停在3樓的情況。根據(jù)檢驗LTL描述的屬性出現(xiàn)的反例路徑，如圖6所示。

根據(jù)反例路徑結(jié)合無錯誤路徑給出的LTL性質(zhì)可知該系統(tǒng)的一個可用測試用例為：該乘客發(fā)出去3樓的信號，最終電梯會停留在3樓，因此得到測試用例如表1所示。