2017, Vol. 28
2. 内蒙古大学 网络信息中心, 内蒙古 呼和浩特 010021
2. Centre of Network and Information, Inner Mongolia University, Hohhot 010021, China
随着Internet的迅速发展, 互联网研究领域中出现了各种各样的软件系统, 且系统的规模、复杂性、分布性和并发性等不断增长.如何保障系统的正确性、安全性和可靠性成为目前需要高度关注和亟需解决的问题, 特别是一些安全关键系统, 若在其运行期间出现错误, 可能会造成巨大的经济或人力损失, 甚至产生灾难性的后果.因此, 需要通过测试来保证系统的正确性.其中, 基于形式化方法进行测试是当前比较流行的一种确认技术.形式化方法是指建立在严格数学基础上的软件系统建模方法, 其目的是刻画系统的行为, 以便在基于形式化模型对复杂系统进行测试生成时, 不至于产生太多冗余的测试例, 以提高测试效率.
在对软件系统进行测试时, 尤其是复杂的软件系统, 存在的大量测试数据或诸多并发行为等因素都可能会使软件系统形式化模型的状态空间非常庞大, 从而导致测试执行效率较低甚至产生状态空间爆炸等问题.并且, 当基于互联网运行软件时, 环境的不可预测也可能会导致系统执行的动态性, 进而导致对于系统的测试不能像有些系统可以预先推导出测试并逐步执行, 而是需要依据现实环境中当前的执行结果进行测试的执行.因此, 如何应对被测动态的输出以进行高效的测试执行就成为问题.
一般软件测试过程至少包括测试生成、测试执行和测试判定3个阶段, 其中, 测试生成和测试执行是独立进行的, 这使得测试耗时长、效率低、代价大以及测试例出现冗余等.基于形式化方法进行测试生成可以使测试生成借助一些成熟的数学方法进行推导, 能够保证一定的测试覆盖; 缺点是建模需要时间, 并且需要有将推出的测试序列向具体的测试例转换的时间.有限状态机、进程代数及Petri网等是常用的形式化建模方法, 着色Petri网(coloured Petri net, 简称CPN)是一种高级Petri网, 它能够更加直观、准确地刻画并发、同步或异步等动态的系统行为, 非常适合对大型复杂的软件系统进行建模和仿真.CPN Tools[1]是一种成熟的Petri网建模和仿真工具, 它的出现为基于CPN的研究提供了可靠的、易使用的仿真平台.而且在采用CPN形式化建模方法建模时, CPN Tools工具会自动进行语法和类型的检查, 用户可根据其提供的错误信息快速建立正确的模型.on-the-fly方法是一种局部模型检测, 是根据待验证模型性质的需要, 有一定针对性地以需求驱动的方式构建状态空间, 在找到反例之前只产生部分或必要的系统状态, 避免对整个状态空间进行穷举搜索[2].该方法不仅能够解决内存和时间不足的问题, 而且还可以减少或避免出现状态空间爆炸问题.根据on-the-fly模型检测的思想, 将on-the-fly方法用于软件测试中, 即通过测试目的从系统规约状态空间中构建待搜索的状态空间, 并对生成的状态空间进行遍历得到测试例, 进而完成对待测软件系统的测试.在实际应用中, 尤其是复杂的并发系统, 可以采用层次化CPN建模方法.所谓层次化CPN建模是指用一些子网来代替需要进一步细化的变迁, 这样做一方面能够使模型的结构更加清晰, 另一方面也便于对模型进行形式化分析.此外, on-the-fly测试方法将测试生成和测试执行同时进行, 不仅可以实时应对并发过程中的不确定性, 而且可以减少测试例冗余, 提高测试效率.因此, 本文提出将on-the-fly测试方法与CPN形式化建模方法相结合, 生成并执行测试例.
本文主要贡献在于:在测试用例生成过程中, 采用CPN建模与on-the-fly测试相结合的方法.利用CPN中的层次概念, 对被测系统实现从整体到局部、由粗到精的逐步细化, 使建模更加清晰; 利用CPN Tools工具建立和执行模型, 并对模型进行安全性、活性等属性的验证; on-the-fly测试方法的引入避免了对整个状态空间的搜索, 在很大程度上可以减少时间和内存的使用, 同时提高测试例生成和执行的效率.
本文第1节介绍一些基本概念.第2节概述CPN建模方法与on-the-fly测试方法的相关研究工作.第3节给出基于CPN的on-the-fly测试方法.第4节以学籍管理系统为例, 说明本文方法的可用性和有效性.第5节进行总结并展望未来工作.
1 前导知识Petri网(Petri net)是一种对离散并行系统的数学表示方法[3, 4], 是描述具有分布、并发、异步特征系统的有效工具, 但其在描述复杂系统时容易面临状态空间爆炸问题, 因而只适用于简单系统的建模.CPN是基于Petri网提出的一种高级Petri网, 它保留了基本Petri网的分析验证方法, 同时对其语义进行了扩展, 增加了颜色集.颜色集的引入可在一定程度上缓解状态空间爆炸等问题[4].下面是着色Petri网的定义[5, 6].
定义 1.着色Petri网是一个九元组, CPN=(Σ, P, T, A, N, C, G, E, I), 满足以下条件.
(1) Σ是一个非空有限类型集, 也称为颜色集, 它决定用于CPN中的token的类型、运算和函数, 例如初始化表达式、弧表达式、防卫函数等;
(2) P是库所的有限集合;
(3) T是变迁的有限集合;
(4) A是有向弧的集合, 满足A⊆P×T∪T×P, 且P∩T=P∩A=T∩A=Ø;
(5) N是节点函数, 定义从A到P×T∪T×P的映射关系, 且弧连接的必须是不同类型的节点, 即(库所, 变迁)或(变迁, 库所);
(6) C是颜色函数, 定义从P到Σ的映射关系, 即C把每个库所p都映射到一个颜色集C(p).换言之, 库所中的每个标识都必须属于某个颜色集;
(7) G是防卫函数, 定义从T到表达式的映射关系, 且满足:∀t∈T:[Type(G(t))=B^Type(Var(G(t)))∈Σ], 其中, B表示布尔值, G(t)中所有变量的类型必须包含于Σ中.Type(expr)表示表达式expr的类型, Type(v)表示变量v的类型, Var(expr)表示表达式expr中变量的集合.当且仅当变迁的防卫函数为真时变迁才可能被触发.若防卫函数为空, 则默认为真;
(8) E是弧表达式函数, 定义从A到表达式的映射关系, 且满足:∀a∈A:[Type(E(a))=C(p(a))MS^Type(Var(E(a)))⊆Σ], 其中, p(a)是N(a)的库所, 表达式的类型是C(p(a))MS.C(p(a))MS表示颜色集C(p(a))上的多重集[7], E(a)的每个求值都生成一个与相邻库所颜色集类型相同的多重集.此外, 弧表达式也可以不出现, 默认为空;
(9) I是初始化函数, 定义从P到闭表达式的映射关系, 且满足:∀p∈P:[Type(I(p))=C(p)MS], 即I把每一个库所p∈P都映射到一个闭表达式, 且闭表达式的类型为C(p)MS.所谓闭表达式是不含任何变量的表达式.
为说明CPN的形式化定义, 以一个简单协议传输为例[8].图 1为简单协议的CPN模型, 其多元组表示形式如图 2所示.
|
Fig. 1 An example of CPN model of simple protocol 图 1 简单协议的CPN模型示例 |
在系统模型构建完成后, 通过执行模型并生成系统模型的状态空间, 即可达图(reachability graph).CPN中的可达图与基本Petri网中的可达树类似, 其核心思想是构造一个包含系统模型执行过程中的所有状态和触发序列的图.在可达图中, 节点表示CPN模型中描述系统的一个可能的状态, 弧表示CPN模型中可能发生的变迁, 该变迁能够触发被测系统状态的改变.图 3为图 1中CPN模型仿真运行后得到的可达图.通过可达图可以对CPN的有界性、可达性和活性等属性进行分析.
本文在基本Petri网可达图的基础上, 依据需求对可达图概念进行扩展.
定义 2. CPN的扩展可达图是一个有向图G=(V, E, R, v0), 其中, V={v0, v1, …, vn}是可达节点的集合, 每个节点vi对应CPN模型可达图中的一个状态; E={e0, e1, …, em}是有向弧集, ei表示由一个可达节点到另一个可达节点的有向弧; R={t0, t1, …, tm}是转换关系集, R:E→V×V, ti是弧上的旁标, 且每个ti对应CPN模型中的一个变迁; v0是扩展可达图的初始节点, 扩展可达图的终点为G中没有出弧的节点, 可能不唯一.
针对图 3所示的可达图, 根据定义2对其进行扩展, 可得该模型的扩展可达图的多元组表示, 如图 4所示.
2 相关工作
CPN形式化建模方法可用于网络协议、软件系统的建模与测试等方面.文献[9]对于软件定义网络的核心协议OpenFlow的交互属性进行层次CPN建模, 并基于模型给出两种测试生成方法进行测试例的推导.文献[10]分析、研究了Minix3操作系统的源码, 并采用CPN的形式化建模方法, 基于属性, 对操作系统调用进行了建模和测试研究.文献[11]中对并行软件系统采用CPN形式化方法建模, 针对模型状态空间规模较大的问题, 提出基于迹等价的化简模型的算法, 在不影响测试结果的情况下缩小模型状态空间并提高测试效率.文献[12]中将CPN用于软件系统性能测试方面, 使用LoadRunner性能测试工具获取Web应用软件中的相关性能参数, 利用得到的参数表及参数公式, 评价系统的性能是否符合最初的开发需求.文献[13]中提出了一种基于CPN的语义Web服务组合的验证与测试方法, 达到了较好的效果, 但是针对复杂的服务组合流程, 可能会产生状态爆炸等问题.本文研究工作与文献[9-13]相比, 虽然都是用CPN进行建模, 但是被测不同, 建模侧重点不同.就测试生成方法而言, 上述文献并没有考虑依据被测执行过程中可能产生的反馈进行测试生成.
基于形式化方法进行测试的常规方法是建模、基于模型进行测试生成, 可能会遇到状态空间爆炸问题和测试例生成过程的复杂性等问题, 为了减少存储并避免出现状态空间爆炸问题, Jean-Claude Fernandez等人首次提出on-the-fly方法的原型[14], 将验证中的on-the-fly算法应用到软件测试中, 即根据测试目的来选择测试例, 进而得到测试套; 并且利用on-the-fly的思想实现了TGV工具[15].最后, 通过实例证明TGV工具不仅能够实现on-the-fly测试算法, 与手工生成测试例相比, 该工具能够高效地生成更加完整和正确的测试例[16].
在on-the-fly测试中, 进行测试例生成和执行时, 根据逐步的测试执行结果指导状态集的生成[17]; 遍历可达图时, 需要考虑被测实现(implementation under test, 简称IUT)的实际响应, 进行路径选择并动态生成测试例[18].因此, on-the-fly测试也可称为基于形式化模型的在线测试, 以区别于测试生成和测试执行分开的离线测试.在测试运行时, 也可以通过基于一个动态变化的概率分布选择动作, 并提供用户指导的测试场景控制[19], 测试时只需考虑实际执行过程的动作序列.on-the-fly测试中通过直接观察具体的输出来指导相应的测试例生成, 而不是预想系统的可能输出提前编写测试例[20].图 5是一种on-the-fly测试机的架构, 在测试过程中, 通过观察被测系统的实际响应来减少需要搜索的状态空间, 即测试驱动部分能够将测试模型部分产生的触发刺激输入给被测系统, 并能够接受被测系统的反馈, 使测试工作依据被测系统的具体反馈进行下一步操作[21, 22].on-the-fly测试的目标是根据被测系统的实际响应减少需要考虑的状态数和变迁数.
|
Fig. 5 The architecture of on-the-fly tester 图 5 On-the-Fly测试机架构 |
On-the-Fly测试最初应用于简单系统的测试[23], 随着对on-the-fly测试算法的不断改进, 现已应用到含有实时和并发的系统中.在测试实时系统时, 微软研究所将on-the-fly测试算法集成在基于模型的测试工具Spec Explorer中, 使用的建模语言是AdmL或Spec#, on-the-fly测试的实现是根据动作的权重和动态改变的策略, 选择实时系统的控制动作.使用Spec Explorer对聊天室系统进行测试时, 发现该工具得出的部分结果与预期结果不符, 其原因是模型的错误与IUT的代码错误, 说明该工具设计的模型有待完善[19].此外, UPPAAL TRON[18]支持对实时系统的on-the-fly测试, 它是对on-the-fly验证工具UPPAAL进行扩展得到的.文献[18]通过使用UPPAAL TRON工具对简单实时系统鼠标单击系统执行on-the-fly测试; 又通过对复杂实时系统火车门控制器的测试, 说明UPPAAL TRON能够解决更多实际问题.同时发现, 在测试实时系统时, IUT和环境的时钟匹配困难, 说明对于IUT和环境的时间同步还存在问题.Lars Frantzen等人实现了基于符号变迁系统形式化建模方法的on-the-fly测试, 开发了Jambition工具, 对Alarm Dispatcher eHealth服务系统进行验证和测试, 并将自己方法的测试结果与传统测试结果进行比较, 发现使用on-the-fly测试方法可以极大地减少测试例的设计和生成成本.但是由于测试数据选择的随机性, 使得测试覆盖度较低, 不能遍历模型中的每一个状态节点和变迁[20].在对Web应用系统或并发系统的测试方面, 如何确保与系统规约的一致性以及如何自动生成测试例都是测试的研究重点.文献[24]基于自动机理论为Web应用提出一种on-the-fly测试方法.其中, Web应用和测试目的使用有限状态机(finite state machine, 简称FSM)建模, 用于选择测试用例.实验结果表明, on-the-fly测试方法中的同步乘积算法在一定程度上减少了发生状态空间爆炸的可能性, 但在执行两个FSM模型的同步乘积运算时复杂度较大.
文献[25]通过使用NModel工具对分布式Web应用系统进行基于模型的on-the-fly测试, 实验结果表明, 基于模型的on-the-fly测试可以发现传统测试中不能发现的错误.但是, 其缺点是对Web应用系统的建模比较耗时, 而且建立测试框架的过程比较复杂.文献[26]的作者van Weelden等人使用自己开发的GAST工具对Java小程序(smart card applet)进行on-the-fly测试, 结果表明, 该工具可以实现on-the-fly测试, 并可自动发现错误.
通过以上分析可以发现, 在对on-the-fly的测试研究中, 已有与自动机、标记变迁系统等形式化方法结合的应用, 但与CPN结合进行on-the-fly测试的研究还很少.与其他形式化建模方法相比, CPN形式化建模方法能够很好地支持对复杂和并发系统的建模, 并支持图形化; 而且CPN Tools工具能够实现对模型的检查和仿真模拟, 并可自动生成和分析完整或部分状态空间.利用CPN形式化建模方法能够保证模型在安全性、活性方面正确性的优势, 将其与on-the-fly测试方法相结合, 不仅可以保障形式化建模时所要求的属性, 也可以利用on-the-fly测试方法简化CPN模型的搜索状态空间, 并可以对动态、实时甚至不确定的系统进行测试生成及执行.
3 基于CPN的on-the-fly测试方法 3.1 相关概念 3.1.1 系统规约系统规约是基于需求规约描述被测系统的抽象模型, 该模型能够预测每个特定状态下被测系统对将要发生的事件的可能响应[27].系统规约中规定了系统应该做什么和不应该做什么, 同时它也是验证被测系统是否正确的依据[28].根据定义2可以得到系统规约扩展可达图的定义.
定义 3.系统规约的扩展可达图是一个有向图S=(VS, ES, RS, v0S), 其中, VS是有限节点集, ES是弧集, RS是关系集, v0S是初始节点, 各个集合的解释与定义2类似.
3.1.2 测试目的测试目的是指测试人员欲测试的被测系统的某一具体的功能, 是使用形式化方法对被测系统中的部分行为的描述, 这些行为一般是系统规约动作集中不完整的动作序列.测试目的的使用可以帮助测试人员在保证错误覆盖可接受的情况下减少生成测试例的数量, 从而在一定程度上降低发生状态空间爆炸问题的可能性.测试目的模型可以根据设计的测试目的建模得到, 也可以从完整的被测系统规约模型中获取.本文中需要构建被测系统的系统规约模型, 因此, 测试目的扩展可达图是在已建好的系统规约扩展可达图的基础上保留需要的节点及与之相关的弧而得到的.
定义 4.测试目的的扩展可达图是一个有向图TP=(VTP, ETP, RTP, v0TP), 其中, VTP是有限节点集, ETP是弧集, RTP是关系集, v0TP是初始节点, 各个集合的解释与定义2类似.
3.1.3 同步乘积同步乘积是指同时遍历系统规约和测试目的的状态空间, 并从系统规约中选取与测试目的相关的部分状态空间, 进而实现仅对测试者所关心的部分状态空间进行测试例的生成和执行.系统规约扩展可达图与测试目的扩展可达图经同步乘积后, 得到的同步乘积扩展可达图即为后续测试过程中需要搜索的状态空间.为描述本文的方法, 下面给出同步乘积扩展可达图的概念.
定义 5.同步乘积的扩展可达图是一个有向图SP=(VSP, ESP, RSP, v0SP), 其中, VSP是有限节点集, ESP是弧集, RSP是关系集, v0SP是初始节点, 各个集合的解释与定义2类似.且满足如下条件.
(1) RSP⊆RS或RSP⊆RTP, 即同步乘积的关系集包含于系统规约(或测试目的)的关系集;
(2) 初始节点v0SP=(v0S, v0TP), 其他节点为vSP=(vS, vTP).在同步乘积扩展可达图中, 每个节点都是由系统规约和测试目的中的节点组合构成的二元组;
(3) 假设vnS为S的终点,
在on-the-fly的测试方法中, 测试例的生成和执行是同时进行的.首先对系统规约扩展可达图和测试目的扩展可达图进行同步乘积得到同步乘积的扩展可达图; 然后根据被测系统的实际响应遍历同步乘积的扩展可达图, 并最终得到测试例.如果被测系统实际运行的行为与遍历同步乘积扩展可达图得到的路径一致, 则测试判定结果为“通过”, 否则为“失败”.若测试执行以“通过”状态结束, 则被测系统通过了该测试例的测试执行.下面给出测试例的扩展可达图的概念.
定义 6.测试例的扩展可达图是一个有向图TC=(VTC, ETC, RTC, v0TC), 其中, VTC是有限节点集, ETC是弧集, RTC是关系集, v0TC是初始节点, 各个集合的解释与定义2类似.
3.2 基于CPN的on-the-fly测试方法On-the-Fly测试方法首先是依据某个测试目的选出测试者关心的那部分系统功能模型, 然后根据被测系统的实际响应来生成测试例, 并且测试例的生成和执行是同步进行的.on-the-fly测试方法的本质是对生成的同步乘积可达图进行遍历, 可以避免传统测试方法中需对整个系统规约状态空间进行遍历以及生成测试例数目多且存在冗余的问题.本文中的on-the-fly测试方法实现过程可以分为3个阶段.
(1) 建模阶段:若系统比较复杂, 可采用层次化的CPN建模.然后使用仿真工具和状态空间工具对系统规约模型进行执行, 生成系统规约的状态空间可达图, 根据定义3对其扩展即可得到系统规约的扩展可达图, 从中选取测试目的得到测试目的的扩展可达图;
(2) 生成同步乘积阶段:运行同步乘积算法, 深度优先遍历系统规约和测试目的的扩展可达图得到同步乘积扩展可达图, 即后续测试过程需要搜索的状态空间;
(3) 生成和执行测试例阶段:以被测系统的实际响应作为遍历同步乘积扩展可达图过程中选择路径的条件, 系统实际执行的路径即为得到的测试例[20].与被测系统的交互过程通过适配器实现.
On-the-Fly测试方法实现过程如图 6所示.
|
Fig. 6 The process of on-the-fly testing method 图 6 On-the-Fly测试方法实现过程 |
3.3 同步乘积算法 3.3.1 同步乘积算法描述
从图 6中可以看出, 同步乘积算法是on-the-fly测试中的核心算法.根据定义3~定义5, 同步乘积算法的工作原理如下.
(1) 若taS:ekS→viS×vjS, tbTP:elTP→vmTP×vnTP, 其中, ekS表示系统规约S中的弧, viS表示ekS的起点, vjS表示ekS的终点, taS表示ekS上的变迁.其余符号定义与此类似, 且taS=tbTP, vnTP不是测试目的的终点, 则有tcSP=taS, tcSP: ehSP→(viS, vmTP)×(vjS, vnTP);
(2) 若taS:ekS→viS×vjS, tbTP:elTP→vmTP×vnTP, 且taS≠tbTP, vnTP不是测试目的的终点, 则有tcSP=taS, tcSP:ehSP→ (viS, vmTP)×(vjS, vmTP).其中, (vjS, vmTP)为同步乘积SP中的当前节点;
(3) 若vnTP为测试目的的终点, 则在系统规约S中搜索从vjS到终点的一条最短路径, 最短路径中的每个节点分别与vnTP组合构成同步乘积SP中的节点, SP中弧上的变迁与系统规约S中相同.
为了更加清晰地理解同步乘积算法, 给出其流程图, 如图 7所示.
|
Fig. 7 The flow chart of the synchronous product algorithm 图 7 同步乘积算法实现的流程图 |
同步乘积算法的伪代码如图 8所示.其中,
|
Fig. 8 Pseudo code of the synchronous product algorithm 图 8 同步乘积算法的伪代码 |
算法输入:系统规约S=(VS, ES, RS, v0S)和测试目的TP=(VTP, ETP, RTP, v0TP).
算法输出:同步乘积SP=(VSP, ESP, RSP, v0SP).
初始化:(1) 同步乘积SP初始节点v0SP=(v0S, v0TP); (2) 将S和TP中所有的弧置为未访问, 且弧的访问次数置为0;(3) viS=v0S, vmTP=v0TP.
根据图 8所示的同步乘积算法的伪代码, 本文使用Java语言编程实现了同步乘积算法.经分析, 该算法在最坏情况下的时间复杂度为O(n3), 空间复杂度为O(n).
3.3.2 同步乘积算法测试为确保算法的正确性, 本节构造两个CPN模型, 实现对该算法的测试, 如图 9和图 10所示.其中, 图 9为含有两个并发变迁的系统规约S1的CPN模型, 图 10为含有3个并发变迁的系统规约S2的CPN模型.模型中涉及的颜色集有整型INT, 变量有整型a.初始库所a1中含有一个token为1`2.
|
Fig. 9 The CPN model of system specification S1 with two concurrencies 图 9 含有两个并发变迁的系统规约S1的CPN模型 |
|
Fig. 10 The CPN model of system specification S2 with three concurrencies 图 10 含有3个并发变迁的系统规约S2的CPN模型 |
根据并发变迁覆盖原则和边界覆盖原则设计了如表 1所示的测试例, 其中涉及的系统规约与测试目的的符号描述见表 2.
|
Table 1 The test cases design of synchronous product algorithm 表 1 同步乘积算法的测试例设计 |
|
|
Table 2 The symbolic description of system specifications and test purposes 表 2 系统规约和测试目的的符号描述 |
利用CPN Tools工具分别执行系统规约S1和S2的CPN模型并生成模型的可达图, 然后扩展系统规约的可达图, 得到其扩展可达图, 分别如图 11和图 12所示.
|
Fig. 11 The extended reachability graph of S1 图 11 系统规约S1的扩展可达图 |
|
Fig. 12 The extended reachability graph of S2 图 12 系统规约S2的扩展可达图 |
同步乘积算法中的测试目的扩展可达图是从已得到的系统规约扩展可达图中选取的, 保留了所需的节点及相关的弧.在测试过程中, 从系统规约S1和S2中分别提取3条测试目的, 见表 2.以TP22为例, 其扩展可达图如图 13所示.
以系统规约S2与测试目的TP22进行同步乘积运算为例, 算法运行结果如图 14所示, 得到的同步乘积SP22的扩展可达图如图 15所示.
|
Fig. 14 The execution result of S2×TP22 图 14 同步乘积S2×TP22的运行结果 |
|
Fig. 15 The extended reachability graph of SP22 图 15 同步乘积SP22的扩展可达图 |
根据表 1中设计的测试例, 分别将系统规约与测试目的进行同步乘积运算, 得到所有测试例的运行结果, 见表 3.
|
|
Table 3 The test results of the synchronous product algorithm 表 3 同步乘积算法的测试结果 |
从表 3中可以看出, 同一系统规约与不同的测试目的进行同步乘积运算后, 得到的同步乘积扩展可达图不同.系统规约扩展可达图中与测试目的相关的路径都在同步乘积扩展可达图中保留, 不相关的路径均已被删除.
此外, 通过分析表 3也可得出结论:同步乘积算法可以实现在系统规约扩展可达图中选择与测试目的相关的部分可达图.而且, 测试目的中是否包含并发变迁以及含有的可并发变迁的不同数量, 都会在一定程度上对生成的同步乘积扩展可达图的规模产生影响.
3.4 结合IUT实际响应的遍历On-the-Fly测试方法实现的第3阶段是生成和执行测试例.其实现过程是在遍历同步乘积扩展可达图的同时, 与IUT进行实时交互, 并根据IUT的实际响应从同步乘积扩展可达图中选择路径, 生成和执行测试例.该过程中, 交互主要包括两个方面.
(1) 将遍历同步乘积的输入, 即触发变迁执行的输入转化为IUT可以接受的输入, 使IUT执行下一步操作;
(2) 将IUT的实际响应转化为CPN模型中的变迁行为, 并将其作为遍历同步积扩展可达图中的选择路径的条件, 驱动遍历过程进一步执行以得到表示被测系统实际行为的路径.
这两种数据传递可以使用一个连接同步乘积遍历过程和IUT的适配器来实现.
4 示例及测试分析学籍管理系统是一种常见的Web应用系统, 具有并发性、实时性和交互性等特点, 本文以其为被测, 示例层次CPN结合on-the-fly的测试方法, 进行测试例的生成和执行.本节首先对被测系统进行建模, 设计不同的场景执行模型并得到各场景的可达图; 然后依据on-the-fly方法的实现过程, 通过适配器实现与被测系统的交互, 生成和执行测试例; 最后, 将得到的测试结果与使用传统测试方法得到的测试结果进行比较和分析.
4.1 学籍管理系统的CPN模型学籍管理系统主要包括两类用户:管理员和普通用户.管理员具有添加、修改和删除的功能, 而普通用户只能查看系统中的信息.系统中的用户均需要登录系统后才能实现相应的功能, 未注册用户不能进入系统.为便于分析问题, 本文对学籍管理系统采用分角色分层次的建模方法, 对系统中添加学生信息模块、查询学生列表模块和按关键字查询学生信息模块等代表性功能模块进行建模.其中, 涉及的库所和变迁的含义见表 4和表 5.模型中涉及的颜色集、变量和函数声明如图 16所示.
|
|
Table 4 The meaning of places in the CPN model 表 4 CPN模型中库所的含义 |
|
|
Table 5 The meaning of transitions in the CPN model 表 5 CPN模型中变迁的含义 |
|
Fig. 16 The statements of the colour sets, variables and functions in the CPN model 图 16 CPN模型中颜色集、变量和函数声明 |
在系统模型的建立过程中, 首先对系统的模型进行整体设计, 建立包含系统各功能模块的顶层模型, 用替代变迁表示各功能, 并在子页中具体实现该功能的详细流程, 进而形成系统的层次模型.图 17为学籍管理系统的top顶层模型, 该页中展示了系统中新添加学生、查询学生列表和按关键字查询学生信息等功能的实现流程, 其中包含两个替代变迁newStuInfo和searchStuInfo.
|
Fig. 17 The top level model of student roll management system 图 17 学籍管理系统的顶层模型 |
图 17中的替代变迁newStuInfo和searchStuInfo对应的子页面分别如图 18和图 19所示.图 18中, newStuInfo子页面主要描述管理员添加学生信息操作的过程.图 19中, searchStuInfo子页面主要描述管理员或普通用户根据关键字查询学生信息的操作过程.
|
Fig. 18 The sub-page of substitution transition newStuInfo 图 18 替代变迁newStuInfo子页 |
|
Fig. 19 The sub-page of substitution transition searchStuInfo 图 19 替代变迁searchStuInfo子页 |
4.2 测试生成过程
在完成对学籍管理系统的建模后, 设置不同的场景运行模型, 从而得到模型的可达图.然后使用on-the-fly测试方法对其进行测试生成和测试执行.
一般情况下, m个用户登录系统时, 系统规约的状态可达图是包含顺序和多并发的.本文根据token数量和变迁覆盖原则设计了表 6所示的测试场景.
|
|
Table 6 The design of test scenario of student roll management system 表 6 学籍管理系统的测试场景设计 |
假设已建立系统的CPN模型, 需要在系统中添加一条学生信息, 或根据一条关键字信息查询所有符合要求的学生, 下面分别以场景1和场景2为例, 展示本文的方法.其中, 两种测试场景中均包含了管理员用户添加一条学生信息的行为过程和根据关键字“10”查看符合条件的学生信息的行为过程, 因此, 本文以这两种行为作为测试目的进行测试, 如表 6中TP1和TP2所示.TP1表示管理员用户登录系统后添加学生信息的行为序列, TP2表示管理员或普通用户根据关键字查看学生信息的行为序列.本文中测试目的的扩展可达图是从系统规约扩展可达图中选取的.
场景1:当系统模型中的token为一个管理员用户、一条学生信息和一条关键字信息时, 即模型的“start”库所中有一个token("admin", "pass", true, 1, false)表示有一个管理员用户进入系统, 用户名为“admin”, 密码为“pass”, 其当前状态是未登录; “nStuInfo”库所中有一个token("31309015", "test15", "male", "BeiJing", true)表示待添加学生的相关信息; “info”库所中有一个token("10", true)表示待查询的关键字“10”.利用CPN Tools工具执行CPN层次模型得到该模型的可达图, 并对其进行扩展转化为扩展可达图, 如图 20所示, 其弧上信息仅以变迁名称表示, 受篇幅所限, 其详细信息省略, 下同.
|
Fig. 20 The extended reachability graph of S1 图 20 系统规约S1的扩展可达图 |
从系统规约S1的扩展可达图中选取测试目的得到测试目的扩展可达图TP1和TP2, 如图 21和图 22所示.
|
Fig. 21 The extended reachability graph of TP1 图 21 测试目的TP1的扩展可达图 |
|
Fig. 22 The extended reachability graph of TP2 图 22 测试目的TP2的扩展可达图 |
将系统规约S1分别与测试目的TP1和TP2的扩展可达图作为同步乘积算法的输入, 即通过运行同步乘积算法将系统规约扩展可达图中覆盖测试目的的部分图形选择出来, 并得到同步乘积的扩展可达图S1×TP1和S1×TP2, 如图 23和图 24所示.
|
Fig. 23 The extended reachability graph of S1×TP1 图 23 同步乘积S1×TP1的扩展可达图 |
|
Fig. 24 The extended reachability graph of S1×TP2 图 24 同步乘积S1×TP2的扩展可达图 |
以遍历S1×TP1为例, 需要模拟用户运行学籍管理系统, 并根据其实时响应来选择测试生成和执行的路径.在此过程中, 将会进一步削减同步乘积扩展可达图中关于测试目的的冗余路径和无关路径, 得到满足系统实时响应的测试例.通过适配器驱动学籍管理系统运行的程序截图如图 25和图 26所示.其中, 图 25所示为成功添加学生信息的情况, “同步乘积可达图信息”域中给出了生成的同步乘积可达图的节点信息和弧信息, 以及可达图中的路径数信息等; “程序运行过程”域中给出了测试机与学籍管理系统交互过程中的执行情况; “生成的路径信息”域中给出了生成的路径, 最终得到的路径为“1, 1g2, 2g3, 3g4, 4g6, 5g9, 6g12, 6”.该路径中“12, 6”为同步乘积扩展可达图的终点, 因此, 该路径表示的测试例的判定结果为“通过”.图 26所示为添加学生信息失败的情况, 新添加的学生信息为“31309015, test15, male, Beijing”, 而数据库中已存在学号为“31309015”的记录, 因而添加失败, 最终得到的路径为“1, 1g2, 2g3, 3g4, 4”.由于“4, 4”不是同步乘积可达图的终点, 因此该路径表示的测试例的判定结果为“失败”.
|
Fig. 25 Succeed to add student information 图 25 成功添加学生信息 |
|
Fig. 26 Failed to add student information 图 26 添加学生信息失败 |
场景2:当系统模型中的token为一个管理员用户、一个未注册用户、一条学生信息和一条关键字信息时, 即模型的“start”库所中有两个token("admin", "pass", true, 1, false)和("wuxiao", "upwd", false, 0, false), “nStuInfo”库所中有一个token("31309015", "test15", "male", "BeiJing", true), “info”库所中有一个token("10", true).其中, token ("wuxiao", "upwd", false, 0, false)表示未注册用户, 不能进入学籍管理系统, 其他各token的含义同场景1.利用CPN Tools工具执行CPN层次模型得到该模型的可达图, 并对其进行扩展转化为扩展可达图, 如图 27所示.
|
Fig. 27 The extended reachability graph of S2 图 27 系统规约S2的扩展可达图 |
此场景中的测试目的与场景1中的测试目的相同, 这里不再赘述.将系统规约S2分别与测试目的TP1和TP2的扩展可达图作为同步乘积算法的输入, 即通过运行同步乘积算法将系统规约扩展可达图中覆盖测试目的的部分图形选择出来, 并得到同步乘积的扩展可达图S2×TP1和S2×TP2, 如图 28、图 29所示.
|
Fig. 28 The extended reachability graph of S2×TP1 图 28 同步乘积S2×TP1的扩展可达图 |
|
Fig. 29 The extended reachability graph of S2×TP2 图 29 同步乘积S2×TP2的扩展可达图 |
以遍历S2×TP2为例, 需要模拟用户运行学籍管理系统, 并根据其实时响应来选择测试生成和执行的路径.通过适配器驱动学籍管理系统运行的程序截图如图 30所示.图中各文本域的含义如场景1, 这里不再赘述.场景1中最终得到的路径为“1, 1g2, 2g5, 3g9, 4g12, 5g18, 6g26, 7g34, 7g38, 7g39, 7”, 且“39, 7”为同步乘积扩展可达图的终点, 因此, 该路径表示的测试例的判定结果为“通过”.
|
Fig. 30 Succeed to search student information 图 30 成功查询到学生信息 |
4.3 测试结果分析
从图 23、图 24、图 28和图 29中可以看出, 当系统中用户数增加时, 生成的状态空间明显增大.执行同步乘积后, 可达图的规模有所减小.在此过程中, 削减了系统规约扩展可达图中与测试目的无关的、冗余的路径.在对同步乘积S×TP的扩展可达图进行遍历时, 根据系统的实时响应来选择测试生成和执行路径.最终可以得到满足系统实时响应的测试例.使用本文方法对表 6中设计的测试场景进行测试, 测试结果见表 7.
|
|
Table 7 The test result of on-the-fly testing method 表 7 On-the-Fly测试方法的测试结果 |
使用传统测试方法进行测试时需要遍历系统规约的完整状态空间, 而本文方法只需遍历与测试目的同步乘积后得到的同步乘积可达图即可.针对表 6中的测试场景, 分别采用传统测试方法和on-the-fly测试方法进行测试, 对两种测试方法中需要遍历的状态空间进行比较, 见表 8.
|
|
Table 8 The comparison of the state space to be traversed in traditional testing and on-the-fly testing 表 8 传统测试与on-the-fly测试中的待遍历状态空间比较 |
从表 8中可以看出, 与传统测试方法相比, on-the-fly测试方法可以明显减小待搜索的状态空间的规模.此外, 通过适配器驱动被测系统的执行可以实现测试例的生成和执行同时进行.而文献[9-13]中提到的方法虽然也是基于CPN进行测试生成的, 但这几种方法无论选择哪种测试覆盖标准, 都需要先生成所有的测试序列, 再进行测试执行, 在这一点上与传统测试方法是一致的, 即测试生成过程与测试执行过程是分开的.如果被测系统比较复杂并且具有动态性, 则生成的测试序列可能并不能反映系统实际运行时执行的路径, 因此造成用于实际执行的测试工作效率低.而本文方法中测试生成和测试执行同时进行, 能够在生成测试例的同时运行被测系统, 得到的测试例直接反映了系统运行时的行为过程, 提高了测试效率.
5 结论在on-the-fly测试方法中, 不需要遍历整个状态空间, 而是根据需要搜索部分状态空间.此外, 测试例的生成和执行是同时进行的, 可以减少测试例冗余, 提高测试效率.CPN是一种常用的形式化建模方法, 可以直观地描述系统并发、同步或异步的动态行为, 非常适合对大型复杂的软件系统进行建模和仿真.本文通过on-the-fly测试方法与CPN形式化建模方法的结合使用, 不但充分利用CPN模型的优点, 并使用CPN Tools工具实现对模型的建立、正确性验证和状态空间分析等功能.而且, 引入on-the-fly测试方法后, 通过运行同步乘积算法实现在系统规约扩展可达图中选择含有测试目的的部分可达图, 因而避免了测试生成时对整个状态空间的穷举遍历, 可以减少时间和内存的使用, 进而提高测试例生成和执行的效率.最后, 以学籍管理系统为例, 说明本文方法的可行性和有效性.
自动化执行测试一直是测试追求的目标, 目前在本方法的实现中, 被测系统的建模过程需要采用人工方式, 文中on-the-fly测试方法与IUT实际响应过程的结合部分虽然已可通过适配器实现, 但与具体被测系统相关的部分还需要测试人员编写.而且这两个部分由于和被测密切相关, 采用统一的方式实现非常困难, 因此在未来工作中将对这两部分作进一步的分析研究, 以逐步实现CPN与on-the-fly相结合过程的全自动化.
| [1] |
CPN Tools (version 4.0).http://cpntools.org/ |
| [2] |
Wu LJ, Su KL, Chen QL, Yang ZH. Algorithm research on "On the Fly" model checking temporal logics of knowledge in multi-agent systems. Journal of Computer Research and Development, 2006, 43(8): 1417–1424(in Chinese with English abstract).
[doi:10.1360/crad20060816] |
| [3] |
Petri CA.Kommunikation mit automaten[Ph.D.Thesis].Bonn: Institut für Instrumentelle Mathematik, 1962. |
| [4] |
Murata T. Petri nets: Properties, analysis and applications. Proc.of the IEEE, 1989, 77(4): 541–580.
[doi:10.1109/5.24143] |
| [5] |
Jensen K. Coloured Petri nets: Basic concepts, analysis methods and practical use. In: EATCS Monographs on Theoretical Computer Science.Springer-Verlag, 1992: 65–87.
https://link.springer.com/book/10.1007/978-3-662-03241-1 |
| [6] |
Jensen K. An introduction to the theoretical aspects of colored Petri nets. Lecture Notes in Computer Science, 1994, 803: 230–272.
[doi:10.1007/3-540-58043-3_21] |
| [7] |
Jense K. Coloured Petri nets: A high level language for system design and analysis. In: Advances in Petri Nets 1990.Berlin, Heidelberg: Springer-Verlag, 1989: 342–416.
[doi:10.1007/3-540-53863-1_31] |
| [8] |
Jensen K, Kristensen LM. Coloured Petri nets: Modeling and Validation of Concurrent Systems. Berlin, Heidelberg: Springer-Verlag, 2009.
[doi:10.1007/b95112] |
| [9] |
Dong LL, Li H, He N, Xing Y. Testing OpenFlow interaction property based on hierarchy CPN. In: Proc. of the 21st IEEE Int'l Conf.on Network Protocols (2013ICNP), 2013: 1–2.
[doi:10.1109/ICNP.2013.6733620] |
| [10] |
Li H, Yue JY, Pang B. CPN modeling and testing of system call for Minix3 access control. Journal of Chinese Computer Systems, 2013, 34(12): 2828–2832(in Chinese with English abstract).
|
| [11] |
Sun T.Research on testing method for parallel software based on colored Petri nets[Ph.D.Thesis].Hohhot: Inner Mongolia University, 2012 (in Chinese with English abstract).http://cdmd.cnki.com.cn/Article/CDMD-10126-1013292809.htm |
| [12] |
Li F.The research on performance parameters in modeling for Web application[Ph.D.Thesis].China University of Petroleum, 2011 (in Chinese with English abstract).http://cdmd.cnki.com.cn/Article/CDMD-10425-1011287576.htm |
| [13] |
Su M.Verification and testing method of the sematic Web service composition based on colored Petri net[Ph.D.Thesis].Hohhot: Inner Mongolia Agricultural University, 2014 (in Chinese with English abstract).http://cdmd.cnki.com.cn/Article/CDMD-10129-1014375623.htm |
| [14] |
Fernandez JC, Mounier L. Verifying bisimulations "On the Fly". In: Proc.of the IFIP TC6/WG6.1 the 3rd Int'l Conf.on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques.Amsterdam: North-Holland Publishing Co., 1990, 90: 95–110.
http://www-verimag.imag.fr/PEOPLE/mounier/Papers/Fernandez-Mounier-90.pdf |
| [15] |
Fernandez JC, Garavel H, Kerbrat A, Mounier L, Mateescu R, Sighireanu M. CADP: A protocol validation and verification toolbox. In: Proc.of the 8th Int'l Conf.on Computer Aided Verification.Springer-Verlag, 1996: 437–440.
[doi:10.1007/3-540-61474-5_97] |
| [16] |
Jard C, Jéron T. TGV: Theory, principles and algorithms. Int'l Journal on Software Tools for Technology Transfer, 2005, 7(4): 297–315.
[doi:10.1007/s10009-004-0153-x] |
| [17] |
Mikucionis M, Larsen KG, Nielsen B.Online On-the-fly testing of real-time systems.In: Proc.of the BRICS.2003.https://www.researchgate.net/publication/250285411_Online_On-the-Fly_Testing_of_Real-time_Systems |
| [18] |
Mikucionis M, Sasnauskaite E.On-the-Fly testing using UPPAAL[Ph.D.Thesis].The Kingdom of Denmark: Aalborg University, Department of Computer Science, 2003. |
| [19] |
Veanes M, Campbell C, Schulte W, Kohli P.On-the-Fly testing of reactive systems.Microsoft Research, 2005.https://www.researchgate.net/publication/228910668_On-the-fly_testing_of_reactive_systems |
| [20] |
Frantzen L, Huerta MDLN, Kiss ZG, Wallet T. On-the-Fly model-based testing of Web services with jambition. In: Web Services and Formal Methods.Berlin, Heidelberg: Springer-Verlag, 2009: 143–157.
[doi:10.1007/978-3-642-01364-5_9] |
| [21] |
Peled D. Ten years of partial order reduction. In: Computer Aided Verification.Berlin, Heidelberg: Springer-Verlag, 1998: 17–28.
[doi:10.1007/BFb0028727] |
| [22] |
Vries RGD, Tretmans J. On-the-Fly conformance testing using SPIN. Int'l Journal on Software Tools for Technology Transfer, 2000, 2(4): 382–393.
[doi:10.1007/s100090050044] |
| [23] |
Fernandez JC, Jard C, Jéron T, Viho C. Using on-the-fly verification techniques for the generation of test suites. In: Computer Aided Verification.Berlin, Heidelberg: Springer-Verlag, 1996: 348–359.
[doi:10.1007/3-540-61474-5_82] |
| [24] |
Li L, Qian Z, He T. An approach to testing Web applications on-the-fly. In: Proc. of the Int'l Conf.on Management of e-Commerce and e-Government (ICMECG 2009).IEEE, 2009: 428–431.
[doi:10.1109/ICMeCG.2009.128] |
| [25] |
Ernits J, Roo R, Jacky J, Veanes M. Model-Based testing of Web applications using NModel. In: Testing of Software and Communication Systems.Berlin, Heidelberg: Springer-Verlag, 2009: 211–216.
[doi:10.1007/978-3-642-05031-2_14] |
| [26] |
Weelden AV, Oostdijk M, Frantzen L, Koopman P, Tretmans J. On-the-Fly formal testing of a smart card Applet. In: Security and Privacy in the Age of Ubiquitous Computing.Springer US, 2005: 565–576.
[doi:10.1007/0-387-25660-1_37] |
| [27] |
Jia GP, Zheng GL. Classification of specification method based on software engineering. Software, 1995, 7: 4–10(in Chinese with English abstract).
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5974237 |
| [28] |
Tretmans J.Testing techniques.In: Formal Methods & Tools Group.Faculty of Computer Science.The Netherlands: University of Twente, 2002.https://www.researchgate.net/publication/266038408_Testing_Techniques |
| [2] |
吴立军, 苏开乐, 陈清亮, 杨志华. 多主体系统时态认知规范的“On the Fly”模型检测算法研究. 计算机研究与发展, 2006, 43(8): 1417–1424.
[doi:10.1360/crad20060816]
|
| [10] |
李华, 岳婧媛, 庞楠. Minix3 访问控制的系统调用的 CPN 建模与测试. 小型微型计算机, 2013, 34(12): 2828–2832.
|
| [11] |
孙涛.基于 CP-nets 模型的并行软件测试方法研究[博士学位论文].呼和浩特:内蒙古大学,2012.
|
| [12] |
李峰.Web 应用软件建模过程中性能参数研究[博士学位论文].北京:中国石油大学,2011.
|
| [13] |
苏萌.基于有色 Petri 网的语义 Web 服务组合的验证与测试方法[博士学位论文].呼和浩特:内蒙古农业大学,2014.
|
| [27] |
贾国平, 郑国梁. 基于软件工程的规约方法分类. 软件, 1995, 7: 4–10.
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5974237
|