李麗萍,王娜,唐姍

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

基于過程模擬樹的Web軟件一致性檢測方法

李麗萍,王娜,唐姍

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

隨著大數(shù)據(jù)、云計算的發(fā)展,Web軟件越來越復(fù)雜,人們對其質(zhì)量要求也越來越嚴格。研究了一種Web軟件一致性檢測的方法。針對Web軟件的獨特性質(zhì),研究了Web軟件創(chuàng)建可執(zhí)行模型的方法,動態(tài)模擬系統(tǒng)運行。引入文法的概念,設(shè)計一個模擬器,在模擬過程中動態(tài)檢測可執(zhí)行模型在外部事件(文法描述的)觸發(fā)下的執(zhí)行是否存在不一致現(xiàn)象,整個過程以模擬樹的方式呈現(xiàn)。該方法能在項目初期檢測出模型的設(shè)計與需求的不一致,在一定程度上保證模型的一致性。

Web軟件;模擬樹;活序列圖;上下文無關(guān)文法;一致性檢測

0 引言

軟件測試是保證軟件質(zhì)量和提高軟件可靠性的一種最主要的手段。軟件測試的核心問題是如何在系統(tǒng)無限的輸入狀態(tài)空間中選擇最有效的測試用例以滿足測試需求[1]。Web軟件已成為國計民生、商業(yè)領(lǐng)域以及未來軟件開發(fā)的主導(dǎo)軟件。當前流行并具有廣闊運用前景的“云應(yīng)用”也是Web應(yīng)用。Web應(yīng)用迅猛發(fā)展的同時,也使人們對其質(zhì)量和安全性等要求變得越來越嚴格。隨著大數(shù)據(jù)、云計算的發(fā)展,Web軟件規(guī)模越來越大,形態(tài)也越來越復(fù)雜,如何保證這些Web軟件的質(zhì)量,倍受人們的關(guān)注。但是Web軟件內(nèi)在的動態(tài)性、異構(gòu)性、復(fù)雜性、交互性、組成成分和鏈接的多樣性等使得對Web軟件的建模和測試都十分困難。

另外,Web軟件面對的是全球范圍的龐大用戶群,出于搶占市場的需要,通常采用快速應(yīng)用開發(fā)方式。鑒于目前的軟件測試主要還是依賴測試工程師的直覺和經(jīng)驗,Web軟件的測試被認為是一個耗時的、代價昂貴的過程。許多Web軟件在沒有進行充分測試的情況下就投入運營,質(zhì)量難以保證,投產(chǎn)后錯誤頻發(fā)。據(jù)統(tǒng)計,目前國內(nèi)80%Web軟件的功能測試都是手工進行的,帶有較大的盲目性和不確定性。因此,迫切需要開發(fā)高效的自動驗證和測試Web軟件的新理論、新方法。正確、合理地實施自動化測試,能夠快速、徹底地對Web軟件進行測試,從而保證軟件質(zhì)量,縮短產(chǎn)品發(fā)布周期,節(jié)省項目經(jīng)費。

現(xiàn)有的Web應(yīng)用測試主要有功能測試、性能測試、可用性、兼容性以及安全性方面的測試。目前比較流行的基于模型的測試是根據(jù)被測系統(tǒng)的分析設(shè)計模型及其派生模型(一般稱其為測試模型)產(chǎn)生測試用例[2],屬于功能測試。

但是以往基于模型的測試中,前提大多是假設(shè)模型是正確的,如何確認模型的正確性,如何在軟件開發(fā)初期對系統(tǒng)模型進行有效地模擬和驗證,一直是業(yè)界所關(guān)注的重點。目前模擬技術(shù)主要用于硬件測試,基于模型模擬對Web軟件進行一致性檢驗及測試的工作還比較少?；谀Ｐ偷腤eb應(yīng)用測試中所創(chuàng)建的測試模型大多不可以動態(tài)地模擬系統(tǒng)運行,而且很多方法對模型也沒有進行一致性檢驗。靜態(tài)建模方法對于描述軟件執(zhí)行動作和動態(tài)交互方面時,特別是例如Web軟件這種交互行為比較復(fù)雜的系統(tǒng)時,表達出來的結(jié)果往往錯綜復(fù)雜,難以閱讀和理解[3]。如果模型本身有錯誤的話,那么基于模型生成的測試用例也是錯誤的。這樣生成的測試用例不一定是有效的測試用例。

本文重點研究Web軟件可執(zhí)行模型的構(gòu)造、模型的一致性檢驗。從構(gòu)造Web軟件的可執(zhí)行模型出發(fā),用文法表示外部觸發(fā)事件,模擬系統(tǒng)的運行,在模擬系統(tǒng)執(zhí)行時檢測模型是否存在一致性問題;整個過程以模擬樹的形式呈現(xiàn)。若一致將生成狀態(tài)遷移系統(tǒng),再結(jié)合測試準則可以生成測試用例,這些將是下一步研究的內(nèi)容。

1 相關(guān)工作

1.1 基于模型的Web軟件測試

目前基于模型的Web應(yīng)用測試比較常用的方法是用有限狀態(tài)機、實體-關(guān)系圖、決策表或UML對其進行結(jié)構(gòu)和行為進行建模[4-13],然后研究其測試方法。Kung和Liu等[4-5]為Web應(yīng)用創(chuàng)建了一個包含對象模型、動態(tài)模型和結(jié)構(gòu)模型的形式化測試模型,提出了一種基于對象關(guān)系圖、對象狀態(tài)圖和網(wǎng)頁導(dǎo)航圖等多模型的Web應(yīng)用建模與測試生成方法。Conallen[8]擴展UML對Web應(yīng)用的體系結(jié)構(gòu)進行了建模。文獻[7-8]中采用Statecharts對Web導(dǎo)航、Web元素以及這些元素之間的交互進行了建模。Offutt等[9]分析了構(gòu)成Web應(yīng)用的網(wǎng)頁和軟件構(gòu)件之間的8種連接關(guān)系,提出了一種基于有限狀態(tài)機(FSM)的Web應(yīng)用建模和測試用例生成方法。意大利的Ricca[10]提出用決策表來對Web應(yīng)用中每個頁面的行為進行建模,然后利用基于決策表的測試準則產(chǎn)生測試案例?？娀纯鄣萚12]設(shè)計并實現(xiàn)了一個基于模型的Web應(yīng)用測試系統(tǒng),用FSM構(gòu)造Web應(yīng)用的測試模型,集成了模型轉(zhuǎn)換器、測試目標分析器、測試序列生成器、FSM和測試序列可視化以及Web應(yīng)用測試執(zhí)行引擎等工具。Hamideh等[13]提出了一個基于結(jié)構(gòu)模型的Web應(yīng)用測試方法,先用結(jié)構(gòu)模型表達Web應(yīng)用的靜態(tài)特征,接著使用本體和映射工具自動生成測試用例揭示W(wǎng)eb應(yīng)用的動態(tài)特征。劉曉強等[14]提出了一種基于云計算自動生成Web應(yīng)用系統(tǒng)功能測試的并行測試用例的方法,該方法使用場景流圖和腳本錄制的并行測試腳本生成和基于搜索的測試數(shù)據(jù)生成,產(chǎn)生自動化測試用例集。

這些研究對Web應(yīng)用的形式建模和基于模型的測試有較大的指導(dǎo)作用。但是,每一種方法都有不同的目的,所關(guān)注的Web特性也不一樣。隨著云計算、大數(shù)據(jù)的蓬勃發(fā)展,Web軟件越來越復(fù)雜,過去的研究有的已經(jīng)不能適應(yīng)新的需求和變化,因而急需探討Web軟件的新的測試方法。

1.2 有關(guān)活序列圖的研究

本文擬用活序列圖(LiveSequenceCharts,LSCs)結(jié)合形式化方法為Web軟件創(chuàng)建可執(zhí)行模型,模擬系統(tǒng)的運行。LSCs是一種基于場景可視化的規(guī)約語言,已成功應(yīng)用于許多軟硬件系統(tǒng)的建模[21-22]。LSCs構(gòu)建的模型的優(yōu)勢是可以動態(tài)地模擬系統(tǒng)的執(zhí)行,然而用它描述系統(tǒng)規(guī)約的一個最大缺點是規(guī)約之間可能存在不一致性,特別是對于包含了許多LSCs的復(fù)雜系統(tǒng)。文獻[15-20]中使用模型檢驗(model-checking)的方法將LSCs轉(zhuǎn)換為等價的時序邏輯以檢測LSCs之間的一致性。吳宏[18]使用時序邏輯表達LSC模型,研究了基于LSC的模型檢驗。戴雨婷等[20]用LSC描述基于場景的需求規(guī)格說明,為了能夠驗證設(shè)計模型是否滿足需求規(guī)格說明,抽取LSC中描述的待驗證的CTL性質(zhì),與由設(shè)計模型生成的SMV程序合并到模型檢驗工具進行驗證。Sibay等[21]提出了一種基于場景的語言來支持LSCs的全局圖和存在圖以便更好地建?；跅l件的場景。針對一般的標簽遷移系統(tǒng)(Labeled Transition System，LTS)不能表達既有全局圖又有存在圖的場景,他們提出了一種模型遷移系統(tǒng)(Model Transition System,MTS),將形式模型轉(zhuǎn)換為MTS,然后從MTS可以抽取出精化的行為場景。Guo等[21-22]提出了用LSCs為交互系統(tǒng)創(chuàng)建可執(zhí)行模型,用上下文無關(guān)文法(Context Free Grammar)表示外部觸發(fā)事件,檢測模型的運行在外部事件的觸發(fā)下是否存在一致性問題。他們用一種PLAY-tree模擬系統(tǒng)的整個運行過程。模擬結(jié)果最終將產(chǎn)生狀態(tài)遷移系統(tǒng),然后基于狀態(tài)遷移系統(tǒng)生成測試用例。目前,工作主要還停留在前半部分,基于狀態(tài)遷移系統(tǒng)生成測試用例還在摸索階段。由于他們的研究并不是針對Web軟件,沒有考慮到Web軟件的特點,因而本文參考他們的工作研究了Web軟件模型的一致性檢驗及測試用例生成。從構(gòu)造Web軟件的可執(zhí)行模型出發(fā),對其測試理論和方法展開研究。

2 相關(guān)知識點

2.1 上下文無關(guān)文法

根據(jù)軟件工程的觀點,文法既是一種用于規(guī)定語言結(jié)構(gòu)的“規(guī)約”,又是一種能夠被語法分析程序自動生成器所識別和轉(zhuǎn)換的“程序”。文法的句子生成在軟件測試數(shù)據(jù)自動生成方面一直有著廣泛的應(yīng)用[23-28]。選用合適的編譯器能將精化后的符號文法直接轉(zhuǎn)換為測試腳本,便于測試用例的自動執(zhí)行。本文基于需求規(guī)約用上下文無關(guān)文法(Context-Free Grammar,CFG)表示外部觸發(fā)事件,檢測模型在外部事件觸發(fā)下的執(zhí)行是否符合定義的需求。

定義1上下文無關(guān)文法G是一個四元組(VN, VT,W,P),其中：

(1)VN是一個非終結(jié)符有限集,每個元素v∈VT被稱為一個非終結(jié)符或者一個變量,通常用大寫字母表示。

(2)VT是一個包含所有終結(jié)符的有限集,終結(jié)符通常用小寫字母表示,在本文對應(yīng)一系列外部事件。

(3)W是一個開始變量,用于表示整個系統(tǒng)的開始,它必須是V的一個成員。

(4)P是一個產(chǎn)生式(規(guī)則)的有限集合,每個產(chǎn)生式的形式是A→α,其中A∈VN,α∈(VT∪VN)*。

本文擴展了上下文無關(guān)文法,用其表示系統(tǒng)的外部觸發(fā)事件。

2.2 活序列圖

傳統(tǒng)活序列圖(LSCs)[29]是一種可視化的基于場景的規(guī)約語言,非常適合于描述如Web軟件這樣的交互式系統(tǒng)。用LSCs為系統(tǒng)建模的好處在于模型可以動態(tài)地模擬系統(tǒng)的運行。LSCs是基于MSCs (Message Sequence Charts)的擴展,也是UML順序圖的變形。但是比起后兩者來,LSCs表達力更強而且語義更豐富[17,29]。LSCs在擴展MSCs的基礎(chǔ)上,主要增加了能表達臨時行為的功能,它可區(qū)分系統(tǒng)的強制性行為、可能性行為和禁止行為。

LSCs主要有2種場景圖：全局圖和存在圖,其中全局圖適用于系統(tǒng)的所有運行,存在圖通常描述系統(tǒng)至少有一次運行所能滿足的場景。全局圖語義精確地描述系統(tǒng)的強制性行為。全局圖包含一個前置圖(prechart)和一個主圖(main chart),圖1所示為一個全局圖[20],其中虛線六邊形表示前置圖,下面的實線矩形框是主圖。如果前置圖中的條件滿足的話,那么系統(tǒng)將一定滿足或運行主圖中定義的場景。該強制性行為在系統(tǒng)運行時能明確地告訴用戶什么是期望的行為。存在圖通常描述系統(tǒng)至少有一次運行所能滿足的場景(沒有前置圖)。

圖1 LSC全局圖Fig.1 Universal chart of LSC

LSCs的對象/實例變量用一個帶生命線的矩形框表示,生命線從上到下表示事件發(fā)生的先后順序。生命線上的數(shù)字,表示事件的發(fā)生或者條件,稱為位置。根據(jù)位置號,可以得到事件發(fā)生的先后次序。在圖1中有4個對象：I1,I2,I3,I4,對象I1有3個位置點〈I1,0〉,〈I1,1〉,〈I1,2〉。對象之間的交互用帶箭頭的消息表示,箭頭表示方向。條件用六邊形表示,圖1有2個判定條件Cond1和Cond2。本文假設(shè)在LSC中的所有消息都是同步消息(滿箭頭)。LSC還有許多其他重要的特性,如cut,temperatures等。溫度值可取兩個值hot和cold,hot表示元素必須發(fā)生, cold表示元素也許發(fā)生。LSC通過給消息、條件和位置點分配溫度值來描述它們的強制性程度。例如,對象I1在位置l1發(fā)送消息m1給I2,它在l2接收到消息,如果消息和位置都標識為hot,那意味著I1必須發(fā)送消息m1,消息必須到達并且I2必須接受該消息。如果消息和位置l1被標識為hot,但是位置l2被標識為cold,那意味著I1必須發(fā)送消息m1,消息必須到達,但是I2可以決定是否接受該消息。對于l1、m1和l2,可以有8種不同的組合方式。有關(guān)LSC的詳細介紹可以參考文獻[29]。

3 模型構(gòu)造

針對以往基于模型的Web軟件測試創(chuàng)建的測試模型不可以動態(tài)執(zhí)行,而且沒有進行一致性檢驗的問題,本文主要研究Web軟件可執(zhí)行模型的構(gòu)造、基于文法的句子生成、模型模擬時一致性檢驗、測試準則的設(shè)計、測試用例的生成與測試集的優(yōu)化。整個項目的技術(shù)路線圖如圖2所示。本文重點研究如何為Web軟件創(chuàng)建可執(zhí)行模型,模型模擬時一致性檢驗。測試準則的設(shè)計、測試用例的生成及優(yōu)化等是后續(xù)研究的內(nèi)容。

圖2 Web軟件測試技術(shù)路線圖Fig.2 The Roadmap of Web software testing

本文研究的具體內(nèi)容包括：

(1)可執(zhí)行模型的構(gòu)造,研究如何將可視化建模與形式化相結(jié)合的方法為Web軟件創(chuàng)建可執(zhí)行模型,使其在外部事件的觸發(fā)下能夠模擬系統(tǒng)的運行。因為LSCs的表達能力和形式語義比UML更加豐富,所以選用LSCs為Web軟件構(gòu)建可執(zhí)行模型。

(2)考慮如何基于需求規(guī)約用上下文無關(guān)文法(CFG)表示外部觸發(fā)事件,解析其遞歸特性,研究基于文法的句子生成算法。主要采用了基于文法覆蓋準則的生成算法,每次有選擇性地選取產(chǎn)生式來替換非終端符,使得文法的每個產(chǎn)生式至少被用到1次,句子的生成采用編譯原理的最左推導(dǎo),即從開始符號出發(fā),總是選擇每個句子的最左非終結(jié)符進行替換。

(3)同時將可執(zhí)行模型(LSCs構(gòu)建的模型)和外部觸發(fā)事件(文法模型)輸入到模擬器,研究進行基于場景的模型一致性檢驗的方法。邊模擬邊進行一致性檢驗。

本文基于Web的機票預(yù)訂系統(tǒng)(Web-based Flight Reservation System,WFRS)為例來展示可執(zhí)行模型的建立,主要考慮LSCs的全局圖模型。WFRS的需求模型圖如圖3所示,包括客戶(Customer)、代理(Agency)和航空公司(Airline)3個對象。Customer是外部對象,用揮手的云表示,它將外部或者用戶的輸入發(fā)送給系統(tǒng)。Agency和Airline都有一個狀態(tài)變量conf,conf有3個取值{false, true,abort},分別表示訂單是否已經(jīng)啟動,確認或者終止。本系統(tǒng)有2種類型的機票：可退票和不可退票,用參數(shù)fNo表示。fNo=0表示購買的是不可退換的機票,fNo=1表示購買的是可退換的機票。如果旅客購買的不是打折票,并且航空公司還沒有確認該訂單,顧客可以退票,否則,顧客不能退票。

圖3所描述的WFRS包含幾個不同的場景。圖3(a)、(b)、(c)描述了成功購票的場景行為。圖3(a)顯示了一個顧客想要訂票,顧客發(fā)送訂票消息給機票代理商(Agency),代理商將自己的狀態(tài)變量conf設(shè)置為false,即Agency.conf=false,并且發(fā)送訂購信息給航空公司(Airline),等待航空公司的回復(fù);圖3(b)顯示了航空公司接到了訂票請求,也將自己的狀態(tài)變量conf設(shè)置為false,即Airline.conf=false,將確認消息發(fā)送回代理商。圖3(c)顯示了代理商收到航空公司發(fā)的確認信息,將狀態(tài)變量conf修改為true,即Airline.conf=true。圖3(d)、(e)、(f)描述了取消訂單的場景。圖3(d)描述了客戶想取消訂單,如果這時訂單還沒有被確認,即狀態(tài)變量conf的值為false,則取消信息將發(fā)送到對象Airline;否則,訂單將不能取消。如果狀態(tài)變量conf的值為abort,則將訂單取消信息發(fā)給顧客。圖3(e)描述了如果航空公司收到一個取消訂單請求,同時狀態(tài)變量conf的值仍為false并且所定機票不是打折票,則修改狀態(tài)變量conf的值為abort,并且發(fā)送取消確認消息給對象Agency。圖3(f)描述了航空公司Airline發(fā)送取消拒絕消息給代理商Agency,Agency將該消息發(fā)送給客戶;圖3(g)描述了航空公司Airline發(fā)送取消確認消息給代理商Agency,Agency將該消息發(fā)送給客戶。因為本文采用的是LSCs的全局圖模型,所以只要前置圖中的條件滿足的話,則系統(tǒng)將一定滿足或運行主圖中定義的場景。

圖3 基于Web的機票預(yù)訂系統(tǒng)Fig.3 Web-based f l ight reservation system

為了構(gòu)造Web軟件的可執(zhí)行模型,本文從整體功能層面和交互行為層面為LSCs添加了形式化的操作語義。

定義2(Ls的操作語義)LSCs描述的規(guī)約Ls的操作語義可以被定義為一個遷移系統(tǒng)Ls=(S,s0,E,Δ)。

(1)S是系統(tǒng)一系列可能的對象狀態(tài)集合,Web應(yīng)用的頁面和構(gòu)件都可以看成實例對象。狀態(tài)s∈S可被定義為(RL,φ),其中RL是一系列LSCs當前正在運行狀態(tài)的拷貝版,φ用True或者False表示這個狀態(tài)是否沖突。

(2)s0=(φ,False)是系統(tǒng)的初始對象狀態(tài),表示W(wǎng)eb應(yīng)用的主頁。

(3)E是一系列系統(tǒng)事件,包括外部事件、系統(tǒng)對象之間的內(nèi)部消息,或者定義在LSCs中的隱藏事件,對應(yīng)于Web應(yīng)用中的各種鏈接關(guān)系,如link, redirect,call,build等。

(4)函數(shù)Δ?S×(ε∪E)×S是一組遷移集合。給定當前狀態(tài)s∈S和一個系統(tǒng)事件e∈E,遷移Δ(s,e)將返回一個更新的狀態(tài),表示W(wǎng)eb頁和軟件構(gòu)件之間的關(guān)系。

4 模型一致性的檢驗

基于文法和符號執(zhí)行的測試數(shù)據(jù)生成是目前非常流行的測試方法[23-28]。Godefroid等[23]利用符號文法作為測試輸入,提高了基于搜索的路徑覆蓋度,發(fā)現(xiàn)了系統(tǒng)更多的錯誤。萬勇兵等[24]提出了一種符號化執(zhí)行的實時系統(tǒng)一致性測試生成方法,用符號值代替具體的數(shù)值,充分體現(xiàn)了符號化模型的優(yōu)勢,避免了由于數(shù)據(jù)枚舉所造成的空間爆炸。本文擴展了上下文無關(guān)文法,用符號值代替具體的數(shù)值。

本文基于系統(tǒng)需求用擴展的上下文無關(guān)文法(CFG)設(shè)計外部觸發(fā)事件;在模擬器中輸入Web軟件的LSCs模型和觸發(fā)事件,檢測模型在外部事件觸發(fā)下的執(zhí)行是否符合定義的需求,即是否存在設(shè)計與需求不一致的問題[30]。用模擬樹展示了整個模擬過程,模擬樹的一個分支對應(yīng)于模型運行的一個場景。在外部事件(文法描述)的觸發(fā)下檢測模型的執(zhí)行是否滿足定義運行時的性質(zhì)。若滿足,表示W(wǎng)eb軟件的設(shè)計模型與需求規(guī)約一致,模擬結(jié)果可以生成狀態(tài)遷移系統(tǒng);若不滿足,表示存在不一致問題,可以生成測試反例。

對于本文采用的實例,基于Web的機票預(yù)訂系統(tǒng)(WFRS),其符號文法G=(VN,VT,W,P)表示如下：非終結(jié)符集VN={W,X,Y,A};終結(jié)符集VT={order(fNo),orderConf i rm(fNo),orderAbort(fNo)}; W∈VN是一個開始變量;P是一組產(chǎn)生式規(guī)則,定義如下：

W→XW|ε

X→order(fNo)Y

Y→orderConf i rm(fNo)

Y→orderAbort(fNo)A

A→abortDeny(fNo)|abortConf i rm(fNo)

fNo→0|1

其中,“|”是一個可選操作符。比如,產(chǎn)生式規(guī)則W→XW|ε表示W(wǎng)→XW和W→ε,其中“ε”代表空字。

將Web軟件的可執(zhí)行模型Ls和文法表示的觸發(fā)事件G輸入到模擬器,模擬系統(tǒng)的運行。檢測模型運行在外部事件w∈L(G)的觸發(fā)下是否存在一致性問題。整個過程將以模擬樹的形式呈現(xiàn),可執(zhí)行模型主要用于動態(tài)模擬系統(tǒng)的執(zhí)行,一致性檢驗通過文法句子的解析及可執(zhí)行模型如何響應(yīng)外部事件實現(xiàn)。

定義3(模擬樹)假定Ls是用LSCs描述的規(guī)約模型,G是一個擴展的上下文無關(guān)文法(Ls,G)：

(1)樹中的每一個節(jié)點都是一個ID。

(2)根節(jié)點是(Q0,V0,φ,False),其中Q0是對象一系列初始狀態(tài)的集合,V0是G中的始元變量,空集φ表示在初始狀態(tài)下LSCs還沒有運行;

(3)(Q,W,RL,φ)是模擬樹的一個節(jié)點,該節(jié)點能遷移到它的每個分支的孩子節(jié)點, (Q,eW,RL,φ)→(Q1,W1,RL1,φ1)當且僅當以下兩個條件之一滿足：

①e是一個外部或者終端事件,對于e∈VT, W∈{VT∪VN}*,當條件(Q2,RL2,φ2)∈Δ((Q1, RL1φ1),e)滿足時,(Q1,eW,RL1,φ1)→(Q2,W, RL2,φ2)成立,稱該遷移為終端遷移。

②E是V中的非終端變量,(Q,EW,RL, φ)→(Q,D1···DnW,RL,φ)成立當且僅當E→D1···Dn滿足上下文無關(guān)文法(CFG)中的產(chǎn)生式規(guī)則,這種遷移為非終端遷移。

(4)如下的兩種節(jié)點是葉節(jié)點：

①(Q,W,RL,True)表示一個有沖突的葉節(jié)點;

②(Q,W,RL,False)表示一個成功(沒有沖突)的葉節(jié)點,W可以取值ε。

在定義3中,四元組(Q,W,RL,φ)被引入描述LSC模擬器的一個運行狀態(tài),其中Q是一系列系統(tǒng)中當前的對象狀態(tài),W是CFG句型中未加工部分,RL是LSCs中一系列正在運行的版本,布爾變量φ True或者False表示該狀態(tài)是否是一個沖突狀態(tài)。這里只考慮LSCs模擬期間的super-step模式和super-step狀態(tài)。在super-step模式,LSCs執(zhí)行盡可能多的事件,直到運行的LSC到達一個穩(wěn)定狀態(tài),期間系統(tǒng)除了等待用戶的另一個外部事件觸發(fā)什么都不做。

定義4(模型的一致性檢查)一個Web軟件的設(shè)計模型Ls與需求規(guī)約一致當且僅當模擬樹的所有分支都是成功的分支。模擬樹的一個分支對應(yīng)于模型運行的一個場景。在外部事件(基于規(guī)約描述的文法)L(G)的觸發(fā)下檢測模型的執(zhí)行是否滿足定義的運行時性質(zhì)。若滿足,表示W(wǎng)eb軟件的設(shè)計模型與需求規(guī)約一致,所有分支運行到達成功葉節(jié)點(φ=False);若不滿足,表示存在不一致性,運行將到達模擬樹的葉節(jié)點(φ=True)。

考慮圖3所描述的在線機票預(yù)訂系統(tǒng)的一致性測試,當輸入上下文無關(guān)文法表示的事件時,其LSC運行的模擬樹如圖4所示。本文采用的是最左解析法,即在解析過程中始終對最左面的非終結(jié)符進行替換。模擬樹中實線橢圓表示的狀態(tài)代表內(nèi)部節(jié)點,虛線橢圓表示葉節(jié)點,φ值為true的實線橢圓表示有沖突的葉節(jié)點。用Agency.conf(fNo)和Airline.conf(fNo)的值描述在線機票預(yù)訂系統(tǒng)的對象狀態(tài),fNo=0表示購買的機票是不可退換的,fNo =1表示購買的是可退換的機票。縮寫Q1～Q3表示模擬樹中3個不同的對象狀態(tài)。

圖4 模擬樹Fig.4 The simulation tree

Q1：Agency.conf(fNo)=Airline.conf(fNo)=true

Q2：Agency.conf(fNo)=Airline.conf(fNo)=false

Q3：Agency.conf(fNo)=Airline.conf(fNo)=abort

根據(jù)需求規(guī)定,如果Agency.conf(0)=Airline.conf(0)的值均為true,顧客不能退票;如果此時模擬器收到觸發(fā)事件A(0)→abortConf i rm(0),那么它將到達一個沖突狀態(tài),模擬樹中φ值為true的節(jié)點。類似地,當Agency.conf(1)=Airline.conf(1)= abort時,機票代理商不能拒絕退票,如果此時事件A(1)→abortDeny(1)執(zhí)行,那么模擬樹同樣將遷移到一個沖突狀態(tài)。在WFRS例子中,所有節(jié)點的RL (當前運行的LSC)的取值都為φ,原因有2個：①初始時沒有LSC被激活;②主要關(guān)注LSCs模擬期間的super-step模式和super-step狀態(tài)。super-step模式表示當LSC接收到一個外部事件并且執(zhí)行了所有可能的內(nèi)部事件后,所有運行的LSC將完成執(zhí)行,直到收到下一個外部事件觸發(fā)[29]。

在模擬樹中,對于每一個有限序列W∈L(G)都存在一個對應(yīng)的分支。LSCs模型是否與需求規(guī)約一致取決于模擬樹中所有的分支是否都是成功的分支,即沒有節(jié)點的φ值為真。相反,如果模擬樹中有的分支存在有沖突的節(jié)點,那么表示LSC模型與需求規(guī)約不一致。

判斷LSCs模型與需求規(guī)約一致是遍歷模擬樹,發(fā)現(xiàn)樹中是否有節(jié)點的φ值被置為true。在WFRS中,因為模擬樹中有φ值為true的節(jié)點分支,因而可以判斷它的LSCs模型與需求規(guī)約不一致。

5 結(jié)論與展望

有效測試是保證Web軟件質(zhì)量的一種重要途徑。本文用活序列圖為Web軟件構(gòu)造可執(zhí)行模型,用擴展的上下文無關(guān)文法表示外部事件模擬系統(tǒng)的執(zhí)行,在模型模擬的過程中對模型進行了一致性檢測,若模型一致的話將生成狀態(tài)遷移系統(tǒng)。根據(jù)生成的狀態(tài)遷移系統(tǒng),再結(jié)合各種測試覆蓋準則,可以生成有效的測試用例。該方法的優(yōu)點是可在項目初期檢測出模型的設(shè)計錯誤,使得在需求分析和設(shè)計階段發(fā)生的錯誤能在早期被發(fā)現(xiàn),提前錯誤檢測的進程,從而可降低開發(fā)成本。用文法表示測試用例,其好處在于將以一種統(tǒng)一的方式表達測試用例?；谝恢滦阅Ｐ蜕蓽y試用例及測試用例約簡將是下一步研究的重點。

[1]GELPERIN D,HETZEL B.The growth of software testing [J].Communications of the ACM,1988,31(6)：687-695.

[2]顏炯,王戟,陳火旺.基于模型的軟件測試綜述[J].計算機科學(xué),2004,31(2)：184-187.

[3]李琳,毋國慶,黃勃,等.基于行為模型的需求可視化研究[J].計算機學(xué)報,2013,36(6)：1313-1324.

[4]KUNG D C,LIU C H,HSIA P.An object-oriented Web test model for testing Web applications[C]//Proceedings First Asia-Pacif i c Conference on Quality Software.Washington,DC,USA：IEEE,2000：537-542.

[5]LIU C H.A formal object-oriented test model for testing Web applications[D].Arlington：University of Texas, 2002.

[6]CONALLEN J.Modeling web application architectures withUML[J].CommunicationsoftheACM,1992,42(10)：63-70.

[7]LEUNG K R P H,HUI L C K,YIU S M,et,al.Modeling web navigation by statechart[C]//Proceedings of the 24th International Computer Software and Applications Conference.Washington,DC,USA：IEEE,2000：41-47.

[8]OLIVEIRA D M C F,TURINE M A S,MASIERO P C. A statechart based model for hypermedia applications[J]. ACM Transactions on Information Systems,2001,19(1)：28-52.

[9]ANDREWS A A,OFFUTT J,ALEXANDER R T.Testing web applications by modeling with FSMs[J].Software Systems and Modeling,2005,4(3)：326-345.

[10]RICCA F,TONELLA P.Analysis and testing of web applications[C]//Proceedings of the 23rd International Conference on Software Engineering.Toronto,Ontario,Canada：IEEE,2001：25-34.

[11]UTTING M,PRETSCHNER A,LEGEARD B.A taxonomy of model-based testing approaches[J].Software Testing Verif i cation and Reliability,2012,22(5)：297-312.

[12]繆淮扣,陳圣波,曾紅衛(wèi).基于模型的Web應(yīng)用測試[J].計算機學(xué)報,2011,34(6)：1012-1028.

[13]HAJIABADI H,KAHANI M.An automated model based approach to test web application using ontology[C]//2011 IEEE Conference on Open Systems.New York,NY,USA：IEEE,2011：348-353.

[14]劉曉強,謝筱夢,杜明,等.面向云測試的并行測試試用例自動生成方法[J].計算機應(yīng)用,2015,35(4)：1159-1163.

[15]BONTEMPS Y,HEYMANS P,KUGLER H.Applying LSCs to the specif i cation of an air traff i c control system [C]//Workshop on Scenarios and State Machines：Models, Algorithms and Tools.USA：IEEE,2003.

[16]BUNKER A,GOPALAKRISHNAN G,SLIND K.Live sequence charts applied to hardware requirements specif i cation and verif i cation：A VCI bus interface model[J].Software Tools for Technology Transfer,2005,7(4)：341-350.

[17]TOBEN T,WESTPHAL B.On the expressive power of LSCs[C]//The 32nd Conf.on Current Trends in Theory and Practice of Computer Science.Prague：SOFSEM, 2006：33-43.

[18]吳宏.基于LSC的模型檢驗研究與實現(xiàn)[D].長沙：國防科技大學(xué),2004.

[19]戴雨婷,繆淮扣,梅佳,等.基于LSC模型檢驗的性質(zhì)抽取[J].上海大學(xué)學(xué)報,2012,18(2)：156-162.

[20]SIBAY G E,BRABERMAN V,UCHITEL S,el al.Synthesizing modal transition systems from triggered scenarios[J].IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,2013,39(7)：975-1001.

[21]GUO H F,ZHENG W,SUBRAMANIAM M.L2c2：Logic-based lsc consistency checking[C]//Proceeding PPDP‘09 proceeding of 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming.New York,USA：ACM,2009：183-194.

[22]GUO H F,ZHENG W,SUBRAMANIAM M.Consistency checking for lsc specif i cation[C]//2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering.Washington,DC,USA：IEEE,2009：119-126.

[23]GODEFROID P,KIEZUN A,LEVIN M Y.Grammar-based whitebox fuzzing[C]//PLDI‘08 Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation.Tucson,Arizona,USA：ACM,2008：206-215

[24]萬勇兵,徐中偉,梅萌.一種符號化執(zhí)行的實時系統(tǒng)一致性測試生成方法[J].電子學(xué)報,2013,41(11)：2276-2284.

[25]SOBOTKIEWICZ L P.A new tool for grammar-based test case generation[D].Melbourne：University of Victoria, 2008.

[26]鄭黎曉,許智武,陳海明.基于文法分支覆蓋的短句子生成算法[J].軟件學(xué)報,2011,22(11)：2564-2576.

[27]LIU S Q,LI L P,GUO H F.Generating test cases via model-based simulation[C]//2012 IEEE 13th International Conference on Information Reuse and Integration(IRI). Las Vegas,NV,USA：IEEE,2012：17-24.

[28]李虎,金茂忠,高仲儀,等.上下文無關(guān)文法測試充分性[J].北京航空航天大學(xué)學(xué)報,2003,29(10)：869-872.

[29]HAREL D,MARELLY R.Come,let’s play：Scenariobased programming using LSCs and the play-engine[M]. Secaucus,NJ,USA：Springer-Verlag,2003.

[30]LI L P,HONG H G,SHAN T.An executable model and testing for Web software based on live sequence charts [C]//15th IEEE/ACIS International Conference on Computer and Information Science(ICIS 2016).Okayama Japan：IEEE,2016.

Research on Consistency Checking Method of Web Software Based on Process Simulation Tree

LI Liping,WANG Na,TANG Shan
(School of Computer and Information Engineering,Shanghai Polytechnic University,Shanghai 201209,China)

Along with the development of big data,cloud computing,Web software has become more and more complexity and people have more strict demand for its quality.The theory and approaches of Web software consistency checking was mainly focused on. Aiming at the unique characteristics of Web software,how to create an executable model to simulate system running was studied.By importing the concept of grammar,a simulator was designed to check if the running of the executable model which triggered by the external events(grammar expressed)was whether consistent or not.The whole process was presented by simulation tree.The method can detect the inconsistent of the model’s design and the requirement at the beginning of the project,and guarantee the consistency of the model to a certain extent.

Web software;simulation tree;live sequence chart;context-free grammar;consistency checking

TP3-0

A

1001-4543(2017)01-0049-09

10.19570/j.cnki.jsspu.2017.01.009

2016-07-21

李麗萍(1976—),女,湖南嘉禾人,副教授,博士,主要研究方向為軟件工程、軟件測試、形式化方法。E-mail：liliping@sspu.edu.cn。

國家自然科學(xué)基金(61272036),上海第二工業(yè)大學(xué)校重點學(xué)科建設(shè)項目(XXKZD1604),上海第二工業(yè)大學(xué)校青年項目資助