一种基于模型检测Web应用生成测试用例的方法

李丽萍(上海第二工业大学计算机与信息工程学院,上海201209)

一种基于模型检测Web应用生成测试用例的方法

李丽萍
(上海第二工业大学计算机与信息工程学院,上海201209)

摘要:提出了一种从用户角度以重构Kripke结构建模并测试Web应用的方法。Web应用中的网页、构件及其关系被看成是原子命题,测试覆盖准则被转换为用计算树逻辑(Computing Tree Logic,CTL)表示的陷阱性质(Trap Property),生成的反例可以实例化来构造测试用例。但是一个陷阱性质生成一个反例将导致生成太多的冗余的测试用例,因此给出了一个测试约简规则来减少冗余的测试用例。最终生成的测试序列将满足给定的覆盖准则并没有冗余。

关键词:Web测试;模型检测;测试准则;测试约简;Kripke结构

0　引言

由于Web应用的独特性,使得Web应用的测试比传统的软件测试更复杂。尤其是功能测试,目前还没有比较系统的自动化测试工具,测试大多依靠人的直觉和经验。由于手工测试需要耗费大量的人力和物力资源,Web应用的自动化测试成为亟待解决的问题。模型检测是一种自动化的、基于模型的性质验证方法,开始于一个用户描述的模型,检测用户给定的性质在模型中是否成立。通常,模型是有限状态迁移模型,性质是一些时序逻辑公式。

基于模型检测生成测试用例的方法是当前测试研究的一个重要方向,因为模型检测器输出的反例可以用来构造测试用例,模型检测的过程可以完全自动地进行,并且有有效的软件工具的支持。

Gargantini等[1]提出了一种从SCR需求生成测试序列的方法,针对的是分支覆盖的准则。Ammann 等[2]提出了一种结合模型检测和变异分析生成测试用例的方法。Offutt等[3]提出了几种基于规约生成测试序列的测试准则。Miao等[4]提出了一种基于模型检测,根据覆盖准则验证Web设计模型的方法。

测试集约简是利用一些算法找到与原测试集具有相同覆盖效率的最小测试集。顾静娴等[5]针对回归测试提出了一种基于组件Web软件的测试覆盖准则和测试需求约简方法,并给出了相应的测试准则之间的包含关系。Askarunisa等[6]讨论了一种约简Web用户会话集来减少测试的方法,并在一些常用的Web应用中进行验证。曾红卫等[7]研究了一种测试用例生成的动态监控优化方法:采用时态逻辑公式重写技术缩减测试目标集,删除被新测试用例覆盖的测试目标;同时,在新测试用例加入测试包时对其进行筛选,以消除冗余。Fraser等[8]针对传统测试方法一次生成测试只满足一个覆盖目标,而覆盖目标之间不是独立的、不是对等难度的等问题,通过分析覆盖目标的相似性,提出了一种新的整个测试集的范式演变方法。他们改进遗传算法优化整个测试用例集以达到同时满足所有覆盖目标。

本文扩展了文献[4]的工作,但是建模方法不同。在建模Web应用时,文献[4]使用了一个中间状态tri-r表示“r被激活”,r可以是Web页或构件。本文认为Web页和构件之间的关系如link-q,call-q 和build-q能直接被看成是原子命题。没必要再增加一个中间状态,因为这将使得状态空间更大且建模方法也更复杂。针对模型检测的状态空间爆炸问题,本文定义了一个测试用例约简规则,并相应地给出了测试约简算法。

本文安排如下:第1部分研究了基于模型检测的Web应用建模的方法;第2部分讨论了如何用时序逻辑来表示测试覆盖准则;第3和第4部分讨论了根据反例生成测试序列并给出了一个约简规则;最后得出结论并给出了进一步的研究方向。

1　Web应用的建模

世界各地的用户通过浏览器都能享受Web应用提供的便利。但是,由于Web应用的异构性、动态性、并发性和链接的多样性等特性给Web应用的建模带来了新的挑战。本文主要研究Web应用基于模型检测生成测试用例的方法,只从用户的观点来关注用户与Web应用的交互。一个典型的Web应用由一系列网页和与之相关的软件构件组成,例如:网页中的超链接属性(href)使用户能从当前网页链接(link)到另一个网页;网页也可以通过窗体(Form)的动作属性或超链接调用(call)软件构件的服务;软件构件可以根据用户请求动态地构建(build)一个新的网页作为响应;软件构件之间可以相互调用等等。

定义1Web应用可以用一个Kripke结构K=(S,A,T,L,AP)来构造,

(1)S是一系列网页和构件的集合。

(2)A⊆S是一系列初始状态的集合,设主页(HomePage)是唯一初始状态。

(3)T⊆S×S是状态迁移关系,T必须满足全序关系,即,对每个状态s∈S存在某个s0∈S满足(s,s0)∈T。

(4)L:S→2AP为状态标记函数,L(s)表示状态s下所有为真的原子命题集;AP是一系列包括Web页、构件和请求性质的原子命题。page-网页名/page-构件名标识了对应网页或构件。请求性质描述了是否有请求被激活。对于一个请求q,link-q表示一个网页到另一个网页q的超链接,call-q表示通过发送请求调用一个软件构件(Form中的submit动作或一个对软件构件的超链接),build-q表示根据请求q动态创建构件。

本文以开发的一个小的Web应用程序——在线成绩查询系统(Web Grade View System,WGVS),来描述所提出的方法。用户在主页发出请求,未注册用户只能浏览新闻(News),如果他想查询成绩必须先登录。在用户填完登录信息并点击提交按钮后,登录请求被发送到构件LoginCheck,LoginCheck检查登录信息,如果用户是合法用户,则建立并返回网页StudentView,否则返回登录失败网页LoginFail。通过网页StudentView,学生可以检索个人成绩信息和个人信息。网页Grade提供成绩检索条件输入项,一旦请求被提交,构件GetGrade根据检索条件动态建立学生的成绩单GradeList。类似地,构件GetStudent将动态建立学生的显示个人信息的网页StudentInfo。网页Grade和StudentInfo可以相互访问。在线成绩查询系统WGVS的Kripke结构如图1所示,这里page-,link-,call-,build-都是Web应用的原子命题。可以看出,该种建模方法既简单又清楚。

图1　WGVS的Kripke结构Fig.1 The Kripke structure for WGVS

2　测试准则的性质生成

测试准则规定了软件达到充分测试时测试集必须满足的基本要求。测试准则主要回答以下问题:应该测试什么,怎样达到测试目标,什么时候测试可以停止。模型检测器通过将测试准则时序化为要验证的性质,然后将其取反为陷阱性质,如果某个陷阱性质不满足,它能给出该性质不满足的理由(反例)。反例表示的状态序列证明模型不满足陷阱性质但反过来证明了性质的满足,因此,从反例构造的测试序列可以满足测试覆盖准则。

本文用计算树逻辑 (Computing Tree Logic, CTL)描述要验证的性质,后面均简称CTL,SMV作为自动生成反例的工具[9]。一个CTL公式包含2部分:① 路径量词A和E。A表示从当前状态开始的所有路径,E表示从当前状态开始存在某条路径。②时态运算符X、F、G和U。CTL规定时态运算符是成对出现的。第一个时态符号可以是A或E,第二个时态运算符可以是X、F、G或U。X、F、G、U分别表示下一状态(next)、某一将来的状态(future)、所有将来的状态(globally)以及直到某个状态(until)。CTL公式中的“¬,∧,∨”分别表示“非、与、或”。本文主要关注覆盖准则中的状态覆盖、迁移覆盖和迁移组合覆盖。

2.1状态覆盖

测试用例TS满足状态覆盖当且仅当Web应用模型中的每个状态必须被生成的系统性质至少覆盖1次。状态覆盖产生的性质是可达性(reachability)性质。一个Web网页或构件s的可达性用CTL公式表示为

其陷阱性质表示为

示例WGVS模型的所有可达性质如表1所示。

表1　WGVS的所有可达性性质Tab.1 Reachability properties for WGVS

2.2迁移覆盖

测试用例TS满足迁移覆盖当且仅当Web应用模型中的每个迁移必须被生成的系统性质至少覆盖一次。迁移覆盖产生的性质是活性(liveness)性质, 即Web应用实现了所有的合法导航。根据Web应用的实现模型K,状态s和s0的迁移是(s,link,s0), (s,call,s0),(s,build,s0)。生成活性性质的方法如下。

(1)对于状态s和s0都是Web网页,迁移形式是(s,link,s0),其对应的陷阱性质可以表示为

(2)对于状态s是Web网页,s0是构件,迁移形式是(s,call,s0),其对应的陷阱性质可以表示为

(3)对于状态s是构件,s0是Web网页,迁移形式是(s,build,s0),其对应的陷阱性质可以表示为

示例WGVS模型的所有活性性质如表2所示。

2.3迁移组合覆盖

测试用例TS满足迁移组合覆盖当且仅当Web应用模型中的每个状态s的所有的射出迁移必须被生成的系统性质至少覆盖1次。迁移组合覆盖产生的性质可以看成是安全性(safety)性质。安全性质主要检测一个非法行为是否在任何路径都不会发生,即,检测模型中是否存在非法迁移,做了不该做的事。

表2　WGVS的所有活性性质Tab.2 Liveness properties for WGVS

设状态s带有n条射向si的迁移{(s,ti,si)| i(i=1,2,···,n)},其安全性质的生成方法如下。

(1)如果s是一个网页,则对每个迁移(s,ti,si)| i(i=1,2,···,n),对应一个s对si的链接或请求。

用CTL公式表示的模型中网页s到网页si没有非法的链接为

用CTL公式表示的模型中网页s到网页或构件si没有非法的请求为

(2)如果s是一个构件,则对每个迁移(s,ti,si)| i(i=1,2,···,n),对应一个构件s建立了网页si作为响应。

用CTL公式表示的安全性质“构件s不返回任何非法网页si”为

表3列出了示例WGVS模型所有的安全性质。对于没有射出迁移的状态,如News,Login Fail和Grade List,则不考虑它们的安全性质。

表3　WGVS的所有安全性质Tab.3 Safety properties for WGVS

3　测试用例的生成

模型检测开始于一个用户描述的模型(通常是有限状态迁移系统),检测用户给定的性质在模型中是否有效。模型检测器的输入为描述Kripke结构的模型和要检验的性质,若模型具有给定的性质,则输出true,否则输出false并同时显示违背性质的反例。一个反例是一条起始于初始状态,终止于性质违反的状态的状态迹,可以用于构造测试用例。SMV同时支持CTL或线性时态逻辑(Linear Temporal Logic,LTL)性质的验证[10]。系统模型用SMV特定的语言编程,程序以模块为单位。本文创建了一个使用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将为每个陷阱性质生成一个反例。例如,陷阱性质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

这个反例表示所验证的性质是false,page-Loginpage是true在下一个状态s2,即模型中存在一条从MainPage到LoginPage的路径。可以看出, SMV构造的反例中只显示在下一状态其值改变的变量。例如,state 3.2中显示了page-LoginPage,其值从0变为1,但是忽略了page-News,因为它的值与状态3.1中完全一样。如果提供用户输入的值,从这些陷阱性质生成的反例能较简单地用于构造测试用例。

4　测试用例的约简

早期模型检测的工具都是基于系统状态空间的穷举搜索,以此来判断系统的行为是否满足规约中所规定的属性要求。然而,对于并发系统或构件式系统,由于进程间事件的交织(interleaving)和构件组合效应,系统模型的状态空间往往呈指数倍增长,最终导致内存不能容纳,人们把这种现象形象地称为“状态空间爆炸”问题。基于模型检测的测试最大的缺点是状态空间的爆炸问题,这大大限制了该方法的应用。

我们知道,模型的一个陷阱性质将产生一个反例。但是这样将导致存在大量的冗余的测试用例,因为一个反例可能包含多个性质的违背[7]。如果陷阱性质很多,那么创建对应的反例将耗费很多的时间。并且,一个高效的测试应该用尽量少的测试和尽量短的测试序列总长度来发现尽可能多的错误。然而,找到这样的测试集是一个NP完全问题。

贪心算法在寻找最小化测试集的问题上有启发性意义。该算法在所有的测试用例中首先选择覆盖最多需求的测试用例,丢弃被选中用例覆盖的需求;重复以上过程,直到所有的测试需求都被覆盖为止。第一步,应该避免创建冗余的反例。通常,从反例实例化的测试用例集中包括大量短的测试用例,它们经常是一些长测试用例的前缀或后缀。本文给出了一个约简规则以减少冗余的测试序列。

定义2(测试约简规则) 一个有效的测试序列TS是一系列满足以下条件的状态序列:

(1)TS起始于初始页;

(2)它不是其他测试序列的前缀或后缀;

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

例如,如果性质生成的反例是TS1=s0s1s2s3, TS2=s0s1s2s3s4和TS3=s0s1s2s1s2s3,那么TS1不是测试序列,因为它是TS2的前缀。TS2是测试序列,因为它满足测试约简规则。TS3不是测试序列,因为它包含了状态“s1s2”连续两次。

本文的生成约简测试用例集的算法是基于贪心算法,如下所示:

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应用程序的模型K和根据选定测试覆盖准则生成的陷阱性质集Ω,输出满足选定测试覆盖准则的约简测试用例集Γ。测试覆盖准则可以是适用于Web应用的所有准则,本文只研究状态覆盖、迁移覆盖和迁移组合覆盖。首先将Ω中所有的陷阱性质标记为unvisited,当Ω非空时,根据模型K检测¬P,一旦从反例生成一个新的测试序列,算法即检测这个新的测试序列是否符合约简规则。如果符合,它是一个有效的测试序列,将它并入测试序列集Γ中,否则,去除该冗余的测试序列,并且从集合Ω中删除陷阱性质¬P。重复以上过程直到所有的陷阱性质被检测。最后生成的覆盖示例WGVS所有陷阱性质P1～P21优化的测试序列见表4。

表4　WGVS生成的测试序列Tab.4 The test sequences for WGVS

5　结语

模型检测是一种自动的、基于模型、验证性质的处理方法。本文主要研究了使用模型检测为Web应用生成测试用例的方法。首先从用户的观点重构Kripke结构以建模Web应用。测试覆盖准则被转换为用CTL表示的验证性质,将性质取反以生成反例。一个反例是从初始状态开始到性质被违背状态的状态序列,可被看成测试序列。基于模型检测生成测试用例方法的最大缺陷是状态爆炸问题。因此,本文给出了一个测试约简规则来减少冗余的测试用例。研究更合适、更高效的约简技术是下一步的工作。

参考文献:

[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应用程序的覆盖率准则和测试需求约简[J].东南大学学报:英文版, 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]曾红卫,缪淮扣.优化基于模型检验的测试生成[C]//第六届中国测试学术会议论文集(CTC2010).中国合肥:中国计算机学会容错计算专业委员会,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

文献标志码:A

文章编号:1001-4543(2015)02-0140-08

收稿日期:2015-01-21

通讯作者:李丽萍(1976–),女,湖南嘉禾人,副教授,博士,研究方向为软件工程、软件测试、形式化方法。电子邮箱liliping@sspu.edu.cn。

基金项目:国家自然科学基金(No.61272036)、上海第二工业大学软件工程学科建设项目(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