李建 楊晉吉

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

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

DOIDOI：10.11907/rjdk.161463

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

0引言

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

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

1基于SPIN的測(cè)試用例生成基本思路

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

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

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

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

2.2LTL公式邏輯描述

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

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

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

2.4反例分析

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

3.1電梯系統(tǒng)

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

3.2建模與LTL

3.2.1模型的Promela描述

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

3.2.2LTL性質(zhì)描述

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

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

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

3.2.3驗(yàn)證與結(jié)果

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

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

點(diǎn)擊Verification，選擇use claim，驗(yàn)證性質(zhì)e1，點(diǎn)擊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)行。

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

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

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