李麗萍(上海第二工業(yè)大學(xué)計算機與信息工程學(xué)院,上海201209)

一種基于模型檢測Web應(yīng)用生成測試用例的方法

李麗萍
(上海第二工業(yè)大學(xué)計算機與信息工程學(xué)院,上海201209)

摘要:提出了一種從用戶角度以重構(gòu)Kripke結(jié)構(gòu)建模并測試Web應(yīng)用的方法。Web應(yīng)用中的網(wǎng)頁、構(gòu)件及其關(guān)系被看成是原子命題,測試覆蓋準(zhǔn)則被轉(zhuǎn)換為用計算樹邏輯(Computing Tree Logic,CTL)表示的陷阱性質(zhì)(Trap Property),生成的反例可以實例化來構(gòu)造測試用例。但是一個陷阱性質(zhì)生成一個反例將導(dǎo)致生成太多的冗余的測試用例,因此給出了一個測試約簡規(guī)則來減少冗余的測試用例。最終生成的測試序列將滿足給定的覆蓋準(zhǔn)則并沒有冗余。

關(guān)鍵詞:Web測試;模型檢測;測試準(zhǔn)則;測試約簡;Kripke結(jié)構(gòu)

0　引言

由于Web應(yīng)用的獨特性,使得Web應(yīng)用的測試比傳統(tǒng)的軟件測試更復(fù)雜。尤其是功能測試,目前還沒有比較系統(tǒng)的自動化測試工具,測試大多依靠人的直覺和經(jīng)驗。由于手工測試需要耗費大量的人力和物力資源,Web應(yīng)用的自動化測試成為亟待解決的問題。模型檢測是一種自動化的、基于模型的性質(zhì)驗證方法,開始于一個用戶描述的模型,檢測用戶給定的性質(zhì)在模型中是否成立。通常,模型是有限狀態(tài)遷移模型,性質(zhì)是一些時序邏輯公式。

基于模型檢測生成測試用例的方法是當(dāng)前測試研究的一個重要方向,因為模型檢測器輸出的反例可以用來構(gòu)造測試用例,模型檢測的過程可以完全自動地進行,并且有有效的軟件工具的支持。

Gargantini等[1]提出了一種從SCR需求生成測試序列的方法,針對的是分支覆蓋的準(zhǔn)則。Ammann 等[2]提出了一種結(jié)合模型檢測和變異分析生成測試用例的方法。Offutt等[3]提出了幾種基于規(guī)約生成測試序列的測試準(zhǔn)則。Miao等[4]提出了一種基于模型檢測,根據(jù)覆蓋準(zhǔn)則驗證Web設(shè)計模型的方法。

測試集約簡是利用一些算法找到與原測試集具有相同覆蓋效率的最小測試集。顧靜嫻等[5]針對回歸測試提出了一種基于組件Web軟件的測試覆蓋準(zhǔn)則和測試需求約簡方法,并給出了相應(yīng)的測試準(zhǔn)則之間的包含關(guān)系。Askarunisa等[6]討論了一種約簡Web用戶會話集來減少測試的方法,并在一些常用的Web應(yīng)用中進行驗證。曾紅衛(wèi)等[7]研究了一種測試用例生成的動態(tài)監(jiān)控優(yōu)化方法:采用時態(tài)邏輯公式重寫技術(shù)縮減測試目標(biāo)集,刪除被新測試用例覆蓋的測試目標(biāo);同時,在新測試用例加入測試包時對其進行篩選,以消除冗余。Fraser等[8]針對傳統(tǒng)測試方法一次生成測試只滿足一個覆蓋目標(biāo),而覆蓋目標(biāo)之間不是獨立的、不是對等難度的等問題,通過分析覆蓋目標(biāo)的相似性,提出了一種新的整個測試集的范式演變方法。他們改進遺傳算法優(yōu)化整個測試用例集以達到同時滿足所有覆蓋目標(biāo)。

本文擴展了文獻[4]的工作,但是建模方法不同。在建模Web應(yīng)用時,文獻[4]使用了一個中間狀態(tài)tri-r表示“r被激活”,r可以是Web頁或構(gòu)件。本文認(rèn)為Web頁和構(gòu)件之間的關(guān)系如link-q,call-q 和build-q能直接被看成是原子命題。沒必要再增加一個中間狀態(tài),因為這將使得狀態(tài)空間更大且建模方法也更復(fù)雜。針對模型檢測的狀態(tài)空間爆炸問題,本文定義了一個測試用例約簡規(guī)則,并相應(yīng)地給出了測試約簡算法。

本文安排如下:第1部分研究了基于模型檢測的Web應(yīng)用建模的方法;第2部分討論了如何用時序邏輯來表示測試覆蓋準(zhǔn)則;第3和第4部分討論了根據(jù)反例生成測試序列并給出了一個約簡規(guī)則;最后得出結(jié)論并給出了進一步的研究方向。

1　Web應(yīng)用的建模

世界各地的用戶通過瀏覽器都能享受Web應(yīng)用提供的便利。但是,由于Web應(yīng)用的異構(gòu)性、動態(tài)性、并發(fā)性和鏈接的多樣性等特性給Web應(yīng)用的建模帶來了新的挑戰(zhàn)。本文主要研究Web應(yīng)用基于模型檢測生成測試用例的方法,只從用戶的觀點來關(guān)注用戶與Web應(yīng)用的交互。一個典型的Web應(yīng)用由一系列網(wǎng)頁和與之相關(guān)的軟件構(gòu)件組成,例如:網(wǎng)頁中的超鏈接屬性(href)使用戶能從當(dāng)前網(wǎng)頁鏈接(link)到另一個網(wǎng)頁;網(wǎng)頁也可以通過窗體(Form)的動作屬性或超鏈接調(diào)用(call)軟件構(gòu)件的服務(wù);軟件構(gòu)件可以根據(jù)用戶請求動態(tài)地構(gòu)建(build)一個新的網(wǎng)頁作為響應(yīng);軟件構(gòu)件之間可以相互調(diào)用等等。

定義1Web應(yīng)用可以用一個Kripke結(jié)構(gòu)K=(S,A,T,L,AP)來構(gòu)造,

(1)S是一系列網(wǎng)頁和構(gòu)件的集合。

(2)A?S是一系列初始狀態(tài)的集合,設(shè)主頁(HomePage)是唯一初始狀態(tài)。

(3)T?S×S是狀態(tài)遷移關(guān)系,T必須滿足全序關(guān)系,即,對每個狀態(tài)s∈S存在某個s0∈S滿足(s,s0)∈T。

(4)L:S→2AP為狀態(tài)標(biāo)記函數(shù),L(s)表示狀態(tài)s下所有為真的原子命題集;AP是一系列包括Web頁、構(gòu)件和請求性質(zhì)的原子命題。page-網(wǎng)頁名/page-構(gòu)件名標(biāo)識了對應(yīng)網(wǎng)頁或構(gòu)件。請求性質(zhì)描述了是否有請求被激活。對于一個請求q,link-q表示一個網(wǎng)頁到另一個網(wǎng)頁q的超鏈接,call-q表示通過發(fā)送請求調(diào)用一個軟件構(gòu)件(Form中的submit動作或一個對軟件構(gòu)件的超鏈接),build-q表示根據(jù)請求q動態(tài)創(chuàng)建構(gòu)件。

本文以開發(fā)的一個小的Web應(yīng)用程序——在線成績查詢系統(tǒng)(Web Grade View System,WGVS),來描述所提出的方法。用戶在主頁發(fā)出請求,未注冊用戶只能瀏覽新聞(News),如果他想查詢成績必須先登錄。在用戶填完登錄信息并點擊提交按鈕后,登錄請求被發(fā)送到構(gòu)件LoginCheck,LoginCheck檢查登錄信息,如果用戶是合法用戶,則建立并返回網(wǎng)頁StudentView,否則返回登錄失敗網(wǎng)頁LoginFail。通過網(wǎng)頁StudentView,學(xué)生可以檢索個人成績信息和個人信息。網(wǎng)頁Grade提供成績檢索條件輸入項,一旦請求被提交,構(gòu)件GetGrade根據(jù)檢索條件動態(tài)建立學(xué)生的成績單GradeList。類似地,構(gòu)件GetStudent將動態(tài)建立學(xué)生的顯示個人信息的網(wǎng)頁StudentInfo。網(wǎng)頁Grade和StudentInfo可以相互訪問。在線成績查詢系統(tǒng)WGVS的Kripke結(jié)構(gòu)如圖1所示,這里page-,link-,call-,build-都是Web應(yīng)用的原子命題?？梢钥闯?該種建模方法既簡單又清楚。

圖1　WGVS的Kripke結(jié)構(gòu)Fig.1 The Kripke structure for WGVS

2　測試準(zhǔn)則的性質(zhì)生成

測試準(zhǔn)則規(guī)定了軟件達到充分測試時測試集必須滿足的基本要求。測試準(zhǔn)則主要回答以下問題:應(yīng)該測試什么,怎樣達到測試目標(biāo),什么時候測試可以停止。模型檢測器通過將測試準(zhǔn)則時序化為要驗證的性質(zhì),然后將其取反為陷阱性質(zhì),如果某個陷阱性質(zhì)不滿足,它能給出該性質(zhì)不滿足的理由(反例)。反例表示的狀態(tài)序列證明模型不滿足陷阱性質(zhì)但反過來證明了性質(zhì)的滿足,因此,從反例構(gòu)造的測試序列可以滿足測試覆蓋準(zhǔn)則。

本文用計算樹邏輯 (Computing Tree Logic, CTL)描述要驗證的性質(zhì),后面均簡稱CTL,SMV作為自動生成反例的工具[9]。一個CTL公式包含2部分:① 路徑量詞A和E。A表示從當(dāng)前狀態(tài)開始的所有路徑,E表示從當(dāng)前狀態(tài)開始存在某條路徑。②時態(tài)運算符X、F、G和U。CTL規(guī)定時態(tài)運算符是成對出現(xiàn)的。第一個時態(tài)符號可以是A或E,第二個時態(tài)運算符可以是X、F、G或U。X、F、G、U分別表示下一狀態(tài)(next)、某一將來的狀態(tài)(future)、所有將來的狀態(tài)(globally)以及直到某個狀態(tài)(until)。CTL公式中的“?,∧,∨”分別表示“非、與、或”。本文主要關(guān)注覆蓋準(zhǔn)則中的狀態(tài)覆蓋、遷移覆蓋和遷移組合覆蓋。

2.1狀態(tài)覆蓋

測試用例TS滿足狀態(tài)覆蓋當(dāng)且僅當(dāng)Web應(yīng)用模型中的每個狀態(tài)必須被生成的系統(tǒng)性質(zhì)至少覆蓋1次。狀態(tài)覆蓋產(chǎn)生的性質(zhì)是可達性(reachability)性質(zhì)。一個Web網(wǎng)頁或構(gòu)件s的可達性用CTL公式表示為

其陷阱性質(zhì)表示為

示例WGVS模型的所有可達性質(zhì)如表1所示。

表1　WGVS的所有可達性性質(zhì)Tab.1 Reachability properties for WGVS

2.2遷移覆蓋

測試用例TS滿足遷移覆蓋當(dāng)且僅當(dāng)Web應(yīng)用模型中的每個遷移必須被生成的系統(tǒng)性質(zhì)至少覆蓋一次。遷移覆蓋產(chǎn)生的性質(zhì)是活性(liveness)性質(zhì), 即Web應(yīng)用實現(xiàn)了所有的合法導(dǎo)航。根據(jù)Web應(yīng)用的實現(xiàn)模型K,狀態(tài)s和s0的遷移是(s,link,s0), (s,call,s0),(s,build,s0)。生成活性性質(zhì)的方法如下。

(1)對于狀態(tài)s和s0都是Web網(wǎng)頁,遷移形式是(s,link,s0),其對應(yīng)的陷阱性質(zhì)可以表示為

(2)對于狀態(tài)s是Web網(wǎng)頁,s0是構(gòu)件,遷移形式是(s,call,s0),其對應(yīng)的陷阱性質(zhì)可以表示為

(3)對于狀態(tài)s是構(gòu)件,s0是Web網(wǎng)頁,遷移形式是(s,build,s0),其對應(yīng)的陷阱性質(zhì)可以表示為

示例WGVS模型的所有活性性質(zhì)如表2所示。

2.3遷移組合覆蓋

測試用例TS滿足遷移組合覆蓋當(dāng)且僅當(dāng)Web應(yīng)用模型中的每個狀態(tài)s的所有的射出遷移必須被生成的系統(tǒng)性質(zhì)至少覆蓋1次。遷移組合覆蓋產(chǎn)生的性質(zhì)可以看成是安全性(safety)性質(zhì)。安全性質(zhì)主要檢測一個非法行為是否在任何路徑都不會發(fā)生,即,檢測模型中是否存在非法遷移,做了不該做的事。

表2　WGVS的所有活性性質(zhì)Tab.2 Liveness properties for WGVS

設(shè)狀態(tài)s帶有n條射向si的遷移{(s,ti,si)| i(i=1,2,···,n)},其安全性質(zhì)的生成方法如下。

(1)如果s是一個網(wǎng)頁,則對每個遷移(s,ti,si)| i(i=1,2,···,n),對應(yīng)一個s對si的鏈接或請求。

用CTL公式表示的模型中網(wǎng)頁s到網(wǎng)頁si沒有非法的鏈接為

用CTL公式表示的模型中網(wǎng)頁s到網(wǎng)頁或構(gòu)件si沒有非法的請求為

(2)如果s是一個構(gòu)件,則對每個遷移(s,ti,si)| i(i=1,2,···,n),對應(yīng)一個構(gòu)件s建立了網(wǎng)頁si作為響應(yīng)。

用CTL公式表示的安全性質(zhì)“構(gòu)件s不返回任何非法網(wǎng)頁si”為

表3列出了示例WGVS模型所有的安全性質(zhì)。對于沒有射出遷移的狀態(tài),如News,Login Fail和Grade List,則不考慮它們的安全性質(zhì)。

表3　WGVS的所有安全性質(zhì)Tab.3 Safety properties for WGVS

3　測試用例的生成

模型檢測開始于一個用戶描述的模型(通常是有限狀態(tài)遷移系統(tǒng)),檢測用戶給定的性質(zhì)在模型中是否有效。模型檢測器的輸入為描述Kripke結(jié)構(gòu)的模型和要檢驗的性質(zhì),若模型具有給定的性質(zhì),則輸出true,否則輸出false并同時顯示違背性質(zhì)的反例。一個反例是一條起始于初始狀態(tài),終止于性質(zhì)違反的狀態(tài)的狀態(tài)跡,可以用于構(gòu)造測試用例。SMV同時支持CTL或線性時態(tài)邏輯(Linear Temporal Logic,LTL)性質(zhì)的驗證[10]。系統(tǒng)模型用SMV特定的語言編程,程序以模塊為單位。本文創(chuàng)建了一個使用SMV基于模型檢測生成測試用例的框架。在SMV中,1和0表示true和false,“!,&,|”表示“?, ∧,∨”。由于篇幅所限,這里只給出示例WGVS部分的SMV表示的程序:

MODULE main

VAR

state:{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10};

login:boolean;

page-MainPage:boolean;

page-LoginPage:boolean;

link-News:boolean;

link-LoginPage:boolean;

call-LoginCheck:boolean;

build-StudentView:boolean;

···

ASSIGN

init(state):=s0;

init(login):=0;

init(page-MainPage):=1;

init(page-LoginPage):=0;

init(link-LoginPage):=1;

init(link-News):=1;

init(link-Grade):=0;

init(call-LoginCheck):=0;

init(build-StudentView):=0; ···

next(state):=case

state=s0:{s1,s2};

state=s2:s3;

···

1:state;

esac;

next(login):=case

next(state)=s3:1;

1:0;

next(state)=s0:1;

1:0;

esac;

next(page-LoginFail):=0;

next(page-MainPage):=case

esac;

next(page-News):=case

next(state)=s1:1;

1:0;

esac;

next(link-Grade):=case

next(state)=s4|next(state)=s10:1;

1:0;

esac;

next(call-LoginCheck):=case

next(state)=s2:1;

1:0;

esac;

next(build-StudentView):=case

next(state)=s3:1;

1:0;

esac;

···

–Node coverage

SPEC AG!page-GradeList;–P8

···

–Transition coverage

SPEC AG(page-MainPage-＞!(link-LoginPage&EX page-

LoginPage));–P12

···

–Transition composition coverage

SPEC AG(page-MainPage-＞ !EX!(link-News|link-

LoginPage))–P22

···

SMV將為每個陷阱性質(zhì)生成一個反例。例如,陷阱性質(zhì)P12AG(page-HomePage→ ?(link-LoginPage∧EX page-LoginPage))表示主頁Main-Page沒有鏈接到登錄頁LoginPage,生成的反例如下:

-＞specification AG(page-MainPage→ !(link-LoginPage

∧EX page-LoginPage))is false＜-

–as demonstrated by the following execution sequence

Trace Description:CTL Counterexample

Trace Type:Counterexample

-＞State:3.1＜-

state=s0

login=0

page-MainPage=1

page-News=0

page-StudentInfo=0

page-LoginPage=0

link-Grade=0

link-StudentView=0

link-News=1

link-LoginPage=1

call-LoginCheck=0

call-GetStudent=0

call-GetGrade=0

build-StudentView=0

···

-＞Input:3.2＜-

-＞State:3.2＜-

state=s2

page-MainPage=0

page-LoginPage=1

link-News=0

link-LoginPage=0

這個反例表示所驗證的性質(zhì)是false,page-Loginpage是true在下一個狀態(tài)s2,即模型中存在一條從MainPage到LoginPage的路徑?？梢钥闯? SMV構(gòu)造的反例中只顯示在下一狀態(tài)其值改變的變量。例如,state 3.2中顯示了page-LoginPage,其值從0變?yōu)?,但是忽略了page-News,因為它的值與狀態(tài)3.1中完全一樣。如果提供用戶輸入的值,從這些陷阱性質(zhì)生成的反例能較簡單地用于構(gòu)造測試用例。

4　測試用例的約簡

早期模型檢測的工具都是基于系統(tǒng)狀態(tài)空間的窮舉搜索,以此來判斷系統(tǒng)的行為是否滿足規(guī)約中所規(guī)定的屬性要求。然而,對于并發(fā)系統(tǒng)或構(gòu)件式系統(tǒng),由于進程間事件的交織(interleaving)和構(gòu)件組合效應(yīng),系統(tǒng)模型的狀態(tài)空間往往呈指數(shù)倍增長,最終導(dǎo)致內(nèi)存不能容納,人們把這種現(xiàn)象形象地稱為“狀態(tài)空間爆炸”問題?；谀Ｐ蜋z測的測試最大的缺點是狀態(tài)空間的爆炸問題,這大大限制了該方法的應(yīng)用。

我們知道,模型的一個陷阱性質(zhì)將產(chǎn)生一個反例。但是這樣將導(dǎo)致存在大量的冗余的測試用例,因為一個反例可能包含多個性質(zhì)的違背[7]。如果陷阱性質(zhì)很多,那么創(chuàng)建對應(yīng)的反例將耗費很多的時間。并且,一個高效的測試應(yīng)該用盡量少的測試和盡量短的測試序列總長度來發(fā)現(xiàn)盡可能多的錯誤。然而,找到這樣的測試集是一個NP完全問題。

貪心算法在尋找最小化測試集的問題上有啟發(fā)性意義。該算法在所有的測試用例中首先選擇覆蓋最多需求的測試用例,丟棄被選中用例覆蓋的需求;重復(fù)以上過程,直到所有的測試需求都被覆蓋為止。第一步,應(yīng)該避免創(chuàng)建冗余的反例。通常,從反例實例化的測試用例集中包括大量短的測試用例,它們經(jīng)常是一些長測試用例的前綴或后綴。本文給出了一個約簡規(guī)則以減少冗余的測試序列。

定義2(測試約簡規(guī)則) 一個有效的測試序列TS是一系列滿足以下條件的狀態(tài)序列:

(1)TS起始于初始頁;

(2)它不是其他測試序列的前綴或后綴;

(3)它不包含冗余的頁。

例如,如果性質(zhì)生成的反例是TS1=s0s1s2s3, TS2=s0s1s2s3s4和TS3=s0s1s2s1s2s3,那么TS1不是測試序列,因為它是TS2的前綴。TS2是測試序列,因為它滿足測試約簡規(guī)則。TS3不是測試序列,因為它包含了狀態(tài)“s1s2”連續(xù)兩次。

本文的生成約簡測試用例集的算法是基于貪心算法,如下所示:

Algorithm.GenerateReducedTestCases

input:A model K and a set ? for all trap properties

output:A reduced test suit Γ satisfying selected test criterion

begin

1Γ=?;

2while ?6=?do

3model checking the trap property?P

4if fail then

5 generate a new test sequence λ from the counterexample;

6check λ whether satisfied with the test reduction rule;

7if satisfied then

8Γ=?！葅λ};

9remove the trap property?P from ?;

10end while

11Output(Γ);

12 end

算法輸入Web應(yīng)用程序的模型K和根據(jù)選定測試覆蓋準(zhǔn)則生成的陷阱性質(zhì)集?,輸出滿足選定測試覆蓋準(zhǔn)則的約簡測試用例集Γ。測試覆蓋準(zhǔn)則可以是適用于Web應(yīng)用的所有準(zhǔn)則,本文只研究狀態(tài)覆蓋、遷移覆蓋和遷移組合覆蓋。首先將?中所有的陷阱性質(zhì)標(biāo)記為unvisited,當(dāng)?非空時,根據(jù)模型K檢測?P,一旦從反例生成一個新的測試序列,算法即檢測這個新的測試序列是否符合約簡規(guī)則。如果符合,它是一個有效的測試序列,將它并入測試序列集Γ中,否則,去除該冗余的測試序列,并且從集合?中刪除陷阱性質(zhì)?P。重復(fù)以上過程直到所有的陷阱性質(zhì)被檢測。最后生成的覆蓋示例WGVS所有陷阱性質(zhì)P1～P21優(yōu)化的測試序列見表4。

表4　WGVS生成的測試序列Tab.4 The test sequences for WGVS

5　結(jié)語

模型檢測是一種自動的、基于模型、驗證性質(zhì)的處理方法。本文主要研究了使用模型檢測為Web應(yīng)用生成測試用例的方法。首先從用戶的觀點重構(gòu)Kripke結(jié)構(gòu)以建模Web應(yīng)用。測試覆蓋準(zhǔn)則被轉(zhuǎn)換為用CTL表示的驗證性質(zhì),將性質(zhì)取反以生成反例。一個反例是從初始狀態(tài)開始到性質(zhì)被違背狀態(tài)的狀態(tài)序列,可被看成測試序列。基于模型檢測生成測試用例方法的最大缺陷是狀態(tài)爆炸問題。因此,本文給出了一個測試約簡規(guī)則來減少冗余的測試用例。研究更合適、更高效的約簡技術(shù)是下一步的工作。

參考文獻:

[1]GARGANTINI A,HEITMEYER C.Using model checking to generate tests from requirements specifications[J]. Software Engineering Notes,1999,24(6):146-162.

[2]AMMANN P E,BLACK P E,MAJURSKI W.Using model checking to generate tests from specifications [C]//Proceedings of the Second IEEE International Conference on Formal Engineering Methods(ICFEM’98).Brisbane,Qld:IEEE Computer Society,1998.

[3]OFFUTT A J,LIU S,ABDURAZIK A,et al.Generating test data from state-based specifications[J].Software Testing,Verification&Reliability,2003,13(1):25-53.

[4]MIAO H,ZENG H.Model checking-based verification of webapplication[C]//Proceedingsofthe12thIEEEInternational Conference on Engineering Complex Computer Systems(ICECCS 2007).Washington,D C:IEEE Computer Society,2007.

[5]顧靜嫻,許蕾,徐寶文.基于組件Web應(yīng)用程序的覆蓋率準(zhǔn)則和測試需求約簡[J].東南大學(xué)學(xué)報:英文版, 2010,26(1):36-42.

[6]ASKARUNISA A,RAMARAJ N.An algorithm for test data set reduction for web application testing[J].Neural Network World,2011,21(1):27-43.

[7]曾紅衛(wèi),繆淮扣.優(yōu)化基于模型檢驗的測試生成[C]//第六屆中國測試學(xué)術(shù)會議論文集(CTC2010).中國合肥:中國計算機學(xué)會容錯計算專業(yè)委員會,2010.

[8]FRASER G,ARCURI A.Whole test suite generation[J]. IEEE Transactions on Software Engineering,2013,39(2): 276-291.

[9]GRUMBERG O,LONG D E.Model checking and modular verification[J].ACM Transactions on Programming Languages and Systems,1994,16(3):843-871.

[10]MCMILLAN K L.The SMV system for SMV version 2.5.4[EB/OL].[2014-09-12].http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps.

中圖分類號:TP3-0

文獻標(biāo)志碼:A

文章編號:1001-4543(2015)02-0140-08

收稿日期:2015-01-21

通訊作者:李麗萍(1976–),女,湖南嘉禾人,副教授,博士,研究方向為軟件工程、軟件測試、形式化方法。電子郵箱liliping@sspu.edu.cn。

基金項目:國家自然科學(xué)基金(No.61272036)、上海第二工業(yè)大學(xué)軟件工程學(xué)科建設(shè)項目(No.XXKZD1301)資助

Test Generation for Web Applications Using Model-Checking

LI Li-ping
(School of Computer and Information Engineering,Shanghai Second Polytechnic University, Shanghai 201209,P.R.China)

Abstract:The Kripke structure is reconstructed to model the Web application from the end users’perspective.Web pages,components and request properties are considered a set of atomic propositions.Test coverage criterion is expressed as trap properties in CTL(Computing Tree Logic)so that counterexamples can be instantiated to construct test cases.But it will result in too many redundant test cases that a counterexample for each trap property is generated.So,a test deduction rule is given to resolve this problem.The test sequences finally generated satisfy the coverage criterion and have no redundancy.

Keywords:Web testing;model checking;test coverage;test reduction;Kripke-based