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

李建 楊晉吉

摘要摘要：提出了一種自動生成系統功能測試用例的新方法。該方法使用Promela語言對軟件系統的狀態和行為進行描述建模，使用LTL公式描述測試覆蓋標準，然后將該組LTL公式和描述狀態行為的Promela模型輸入SPIN模型檢測工具，并利用模型檢測工具自動生成相應的證據路徑，最后結合正例將路徑轉化成滿足相應覆蓋標準的系統功能測試用例，并以電梯系統模型對該方法作出了詮釋。

關鍵詞關鍵詞：功能測試用例；SPIN；模型檢測；Promela建模

DOIDOI：10.11907/rjdk.161463

中圖分類號：TP306文獻標識碼：A文章編號文章編號：16727800（2016）007000103

0引言

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

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

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

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

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

采用模型檢測技術對被測系統和測試覆蓋標準進行形式化描述，本文采用Promela描述被測系統，用 LTL 描述測試覆蓋標準。2.1Promela建模

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

2.2LTL公式邏輯描述

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

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

采用形式化公式來表達，即證明M╞是否成立，其中，M表示模型，表示時態邏輯公式。分別將轉換成自動機A，將M轉換成AM，即相當于證明：

2.4反例分析

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

3.1電梯系統

電梯在運行時分為如下3種狀態：①空閑狀態：電梯沒有發出目的層呼叫信號和呼叫電梯信號；②等待狀態：開始響應某一個呼叫電梯的信號，或有乘客正進、出電梯；③運行狀態：正在響應某一個呼叫電梯信號。電梯系統運行模型如圖5所示。

3.2建模與LTL

3.2.1模型的Promela描述

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

3.2.2LTL性質描述

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

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

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

3.2.3驗證與結果

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

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

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

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

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

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