计算机应用   2017, Vol. 37 Issue (5): 1276-1281  DOI: 10.11772/j.issn.1001-9081.2017.05.1276
0

引用本文 

张玮, 孙涛, 万晓云. 针对并行软件待测行为测试的模型化简方法[J]. 计算机应用, 2017, 37(5): 1276-1281.DOI: 10.11772/j.issn.1001-9081.2017.05.1276.
ZHANG Wei, SUN Tao, WAN Xiaoyun. Simplification method for testing behavior of parallel software[J]. Journal of Computer Applications, 2017, 37(5): 1276-1281. DOI: 10.11772/j.issn.1001-9081.2017.05.1276.

基金项目

国家自然科学基金资助项目(61562064,61462066)

通信作者

孙涛, 电子邮箱 cssunt@imu.edu.cn

作者简介

张玮 (1991-), 男, 内蒙古巴彦淖尔人, 硕士研究生, 主要研究方向:软件测试;
孙涛 (1980-), 男, 内蒙古呼和浩特人, 副教授, 博士, 主要研究方向:软件测试, E-mail: cssunt@imu.edu.cn;
万晓云 (1990-), 女, 河北张家口人, 硕士研究生, 主要研究方向:软件测试

文章历史

收稿日期:2016-11-09
修回日期:2017-01-12
针对并行软件待测行为测试的模型化简方法
张玮, 孙涛, 万晓云    
内蒙古大学 计算机学院, 呼和浩特 010021
摘要: 针对并行软件的状态空间规模大导致测试难度大的问题,提出一种基于着色Petri网(CPN)的针对待测行为的并行模型化简方法。首先,将原模型根据模型中出现的并发变迁、同步变迁、分叉库所、汇合库所等特殊节点的个数分成若干个子模块;其次,判断待测行为在模型中的位置,建立待测行为测试集;最后,对每一个并行模块中符合化简条件的非待测行为设定执行优先级。通过对化简前后状态空间分析报告的对比,状态空间中节点的缩减率至少达到40%以上,并且在化简前后对于待测行为生成的全覆盖测试路径不受影响。
关键词: 着色Petri网    并行软件    待测行为    优先级    测试集    全覆盖    
Simplification method for testing behavior of parallel software
ZHANG Wei, SUN Tao, WAN Xiaoyun     
School of Computer Science, Inner Mongolia University, Hohhot Nei Mongol 010021, China
Abstract: Focusing on the issues that it is very difficult to test the parallel software system, and the size of state space is too large, a Colored Petri Net (CPN) model for simplifying the tested behavior of the parallel model was proposed. Firstly, the original model was divided into several sub modules according to the number of the special nodes, such as concurrent transitions, synchronous transitions, the branch places, and the confluence places. Secondly, the position of the tested behavior and the test set was created. Finally, the execution priority was set for the non-test behavior in each parallel module which met the reduction condition. By comparing the results of the state space analysis before and after simplification, the reduction rate of nodes in state space is at least 40%, and the full coverage test path generated by the tested behavior was not affected by the simplification.
Key words: Colored Petri Net (CPN)    parallel software    test behavior    priority    test set    full coverage    
0 引言

随着软件技术和产业的发展,并行软件已经成为常见的软件形式,并且在软件的开发和研究中都占据了十分重要的位置。例如,很多基于网络的软件系统都具有并行性特点,目前备受关注的基于云计算的软件系统和基于物联网的软件系统也不例外[1]

然而,和非并行性软件相比,并行软件的正确性确认更加困难。在并行软件中,各个并行实体具有大量的并行行为,同时各实体间还具有交互协同行为,这就导致了软件执行过程的高度复杂性,软件状态空间规模呈指数增长,其执行规模和处理难度都远远超出了非并行软件[2]

从系统建模的角度而言,着色Petri网 (Colored Petri Net, CPN) 支持可视化建模过程,通过位置、变迁、有向弧、函数式编程语言 (Programming Language, ML) 表达式和托肯 (token) 直接描述系统行为,支持自动仿真执行,允许多token并发运转。也就是说,对于并发、同步及交互行为,直接给出描述即可,多token的并发运转即表达了系统的并发行为和由此而引发的系统状态变化情况[3]。所以,采用CPN描述并行软件时,并行行为的复杂属性并不会导致模型复杂度的提升,尽管并行行为将导致模型的状态空间规模大幅提升,但CPN模型的状态空间是根据模型自动生成的,建模时并不需要考虑系统状态及其变化过程[4]

在并行软件系统测试中,为了限定模型状态空间规模,研究者提出了一些模型化简方法。在文献[5]中提出了基于迹等价的CP-nets的模型化简方法,该方法首先对模型进行被测实现部分和测试模拟环境部分的划分,并将连接两部分的端口位置和端口变迁标记为可观察位置和可观察变迁;其次,提出发生序列的迹的定义; 最后,提出基于迹等价的并行软件模型化简算法,对符合条件的位置、变迁和其他模型元素进行化简,将被化简的功能合并到邻近的模型元素中。该方法虽然最终可以缩减状态空间图的节点,但是规避了模型中的特殊节点,而且当模型足够大时,依然存在空间爆炸的可能性。

在并行软件测试中,每一次测试的测试目的不同,可以选择不同的行为作为待测行为[6], 所以待测行为是指在测试过程中测试人员所指定要测试的某些软件功能行为,其余的则称为非待测行为。例如,可以选择待测软件中与某些数据或资源相关的行为作为本次测试的待测行为。这样,就可以生成覆盖待测行为并行执行全部路径的测试序列[7]。文献[8]中提出一种基于并行软件化简的测试序列生成算法,对模型化简的好处是避免了对并行软件全部状态空间进行搜索和测试。然而,当软件的状态空间规模过大时,生成完全覆盖待测行为的测试序列同样十分困难。

因此,本文提出一种针对并行软件待测行为测试的模型化简方法, 该方法以缩减状态空间规模为目的,采用CPN来形式化描述软件系统的转变,并结合执行对原有模型的分块处理及非待测形为执行顺序的优先级,从总体上减少测试代价,达到测试序列全局优化的目的。设定优先级可以有效降低软件系统中非待测行为的并行复杂度,所以可以有效缩减模型状态空间规模[9]。由于化简操作仅针对并行执行的非待测行为进行了执行优先级设定,而对于待测行为和并发同步交互等特殊节点不作处理,所以化简后再生成覆盖待测行为的测试序列效果不变。通过实验对比和分析,验证了化简前后生成测试序列的一致性和状态空间缩减效率,从而证明了该方法的有效性[10]

1 Petri网定义

定义1    CPN[11]。一个非层次CPN可以定义为一个9元组:

$ CPN = (P,T,A,\mathit{\Sigma },V,C,G,E,I) $

其中:P是一个有限的库所 (Place) 的集合; T是一个有限变迁 (Transition) 的集合,满足PT=∅,即一个节点要么是一个库所,要么是一个变迁; A是有向弧 (Arc) 的集合,满足AP×TT×P,即每一条弧开始于一个库所 (变迁),结束于一个变迁 (库所); Σ是有限非空颜色集 (Color set),用于定义数据类型; V是有限变量 (Variable) 的集合, 对所有变量vV,满足Type[v]∈Σ; C:PΣ是颜色集函数 (Color Set Function),它指定了每个库所颜色集; G:TEXPRV是防卫表函数 (Guard Function),它指定了每个变迁的防卫表达式, 且对于所有的tT,有Type[G(t)]=Bool,即防卫表达式的返回值必须是布尔型。E:AEXPRV,是弧表达函数 (Arc Expression Function),它为每个弧指定了一个弧表达式,且对于所有的aA,有Type[E(a)]=C(p)MS(MS即多重集 (Multi Set)),即弧表达式的类型必须与它相关的库所的类型一致; I:PEXPR,是初始化函数 (Initialization Function),它给每个库所指定一个初始标记,且对于所有的pP,有Type[I(p)]=C(p)MS, 即,初始表达式是一个与库所颜色集相一致的元组。

以上定义为CPN的一个形式化定义,当然除了基本定义以外,本文所提算法还将用到以下定义。

定义2    系统模型 (System Model, SM)。在并行软件测试中,首先根据待测软件的需求规范,建立软件的CPN模型,称此CPN模型为待测的系统模型。

定义3    抑制弧 (Inhibition Arcs)[12],又称抑止弧、约束弧或者禁止弧。带抑止弧的Petri网 (Petri net with inhibition arcs) 是在原型Petri网的基础上增加一种连接库所和变迁的弧形成的。这种弧只对 (在原型Petri网意义下) 具备发生条件的变迁是否允许发生起控制作用,变迁一旦发生,抑止弧对由此引起的标识变化不产生影响。目前抑制弧习惯用带空心圆圈的线段符号表示,如图 1所示,p2t2之间的弧即为抑制弧,作用为当p2有token时,p1库所所在路径不执行,直到p2库所中没有token后再执行这一路径。

图 1 抑制弧 Figure 1 Inhibition arc

定义4    并发变迁 (Concurrent Transition, CT)。在系统模型中,如果一个变迁最多有一个输入弧且有多个输出弧,则这个变迁称为并发变迁。例如图 1t1即为模型的并发变迁。

定义5    同步变迁 (Synchronous Transition, ST)。在系统模型中,如果一个变迁最多只有一个输出弧并且有多个输入弧,则这个变迁称为同步变迁 (ST)。例如图 2t7即为模型的同步变迁。

图 2 节点定义 Figure 2 Node definition

定义6    分叉库所 (Branch Place, BP)。在系统模型中,如果一个库所最多有一个输入弧且有多个输出弧,则这个库所称为分叉库所。例如图 2p9即为模型的分叉库所。

定义7    汇合库所 (Confluence Place, CP)。在系统模中,如果一个库所最多只有一个输出弧且有多个输入弧,则这个库所称为汇合库所。例如图 2p7即为模型的汇合库所。

定义8     同步并发变迁 (Synchronous Concurrent Transition, SCT)。在系统模型中,如果一个变迁有多个输入弧和多个输出弧,则这个变迁称为同步并发变迁。例如图 2t12即为模型的同步并发变迁。

定义9    汇合分叉库所 (Confluence Branch Place, CBP)。在系统模型中,如果一个库所有多个输入弧和多个输出弧,则这个库所称为汇合分叉库所。例如图 2p4即为模型的汇合分叉库所。

定义10    特殊节点 (Special node)。在系统模型中所有的CT、ST、CP、BP、SCT、CBP均称为特殊节点。

定义11    支路 (Branch)。在系统模型中,位于系统模型的每一个子模块中并发变迁 (同步并发变迁) 或分叉库所 (汇合分叉库索) 之后具有单入单出弧的顺序路径称为支路。如图 3所示,其中用圆角矩形所标注的路径即为支路。

图 3 支路与干路模型定义 Figure 3 Model definition of branch and trunk

定义12    干路 (Trunk)。在系统模型中,位于系统模型的每一个子模块中分叉库所 (BP) 或者并发变迁 (CT) 之前具有单入单出弧的顺序路径称为前置干路;位于汇合库所 (CP) 或同步变迁 (ST) 之后的具有单入单出弧的顺序路径称为后置干路;位于分叉库所或者并发变迁之后且在汇合库所或同步变迁之前的具有单入单出弧的顺序路径称为中间干路。如图 3所示,其中最左边直角虚线矩形内所注为前置干路,中间直角虚线矩形标注为中间干路,最右边直角虚线矩形所注为后置干路。

2 算法描述

因为本文算法所针对的模型是控制流模型,所以仅考虑单一初始token的情况。针对待测行为本文分为含有单个待测行为与多个待测行为两种情况来考虑[13]

算法1    系统模型预处理算法。

1) 对系统模型进行深度优先遍历,判断各节点属性, 并将各节点归类。

Begin

void DFS (SM n)        //n代表系统模型中的节点

{

Visited[n]=true;

If (nCommonNode) {

//n为含有非特殊节点 (根据节点的出入弧判断)

    If (nplace){

        Merge (SetPlace[n]);         //将n归为库所集

    } else if (ntransition) {

        Merge (SetTransition[n]);         //将n归为变迁集

    }

} else if (nSpecialNode) {         //n为特殊节点

    if (nplace) {

        Merge (SetCP[n]‖SetBP[n]‖SetCBP[n]);

        //根据n的出入弧条数选择归并到哪一个特殊库所集

    }else if (ntransition) {

        Merge (SetCT[n]‖SetST[n]‖SetSCT[n]);

        //根据n的出入弧条数选择归并到哪一个特殊变迁集

    }

}

}

End

2) 对模型进行分块处理。

Begin

for (i=1;i < =n; i + +) {

    Modular=1;

    if (CT!=NULL‖ST!=NULL‖BP!=NULL‖CP!=NULL)

        + +Modular[];

        Record (Modular[i]);

        //出现特殊节点,模块计数加1,并记录模块信息

    else

        return SM

        //返回模型继续寻找特殊节点,直到将模型分为若干个模块

}

End

3) 判断模型的支路与干路。

Begin

If (CTmodular[n]‖STmodular[n]‖BPmodular[n]‖

    CPmodular[n]‖CBPmodular[n]‖SCTmodular[n]){        //模型中出现特殊节点

    Branch[]+ +;

    Record (Branch[n]);         //记录支路的条数与支路上的信息

    Trunk[]+ +;

    Record (Trunk[n]);         //记录干路的条数与干路上的信息

}else{

    Trunk+ +;

    Record (Trunk[n]);

    //没有特殊节点时仅记录干路条数与干路上的信息

}

End

首先对系统模型的预处理算法实现描述,具体操作如下所述:

第1) 步    对模型中的所有节点进行遍历,并记录每一个节点对应的输入弧与输出弧:

① 当一个节点有一个入弧和多个出弧时,判断此节点是库所还是变迁,如果节点是库所时,则此模型有分叉库所;如果节点是变迁时,则此模型有并发变迁。

② 当一个节点有多个入弧和一个出弧时,判断此节点是库所还是变迁,如果节点是库所时,则此模型有汇合库所;如果节点是变迁时,则此模型有汇合变迁。

③ 当一个节点有多个入弧和多个出弧时,判断此节点是库所还是变迁,如果节点是库所时,此模型中有汇合分叉库所;如果节点是变迁时,则模型有同步并发变迁。

④ 当一个节点有一个入弧和一个出弧时,则此模型为顺序执行。

⑤ 当一个库所只有输出弧没有输入弧时,此库所为初始库所。

⑥ 当一个库所只有输入弧没有输出弧时,此末库所为末库所。

第2) 步    对模型进行分块处理。从模型的初始库所进行遍历,当出现第1) 步中的①~③ 三种特殊节点时,特殊节点之前的路径记为1模块,再从此特殊节点继续遍历,由此节点产生含有分支的路径记为下一模块,如果分支再出现①~③ 三种节点,则此节点是这一模块的终止节点,如果没有出现特殊节点,则这一模块没有嵌套;循环分块,直到遍历到模型的最后一个节点。

第3) 步    判断模型中的干路与支路。如果模型中包含分叉库所或者并发变迁,则此节点之前具有单入单出弧的顺序路径记为前置干路,节点之后的每一条具有单入单出弧的顺序路径记为支路;如果模型中包含汇合库所或者同步变迁,则此节点之后具有单入单出弧的顺序路径记为后置干路,节点之前具有单入单出弧的顺序路径记为支路;如果模型中既包含分叉库所或者并发变迁,又包含汇合库所或者同步变迁,则这对特殊节点之间具有单入单出弧的顺序路径称为中间干路,其余为支路。

算法2    单个待测行为时的算法。

当有单个待测行为时,需要判断待测行为所在模型位置并进行优先级处理 (待测行为处于同一支路或干路)。

Begin

    If (BehaviorTestTrunk){

        Serialization (Branch[]);

                //将支路不在同一路径的非待测行为串行化处理

    } else if (BehaviorTestBranch){

        Sequential (Trunk);        //顺序执行干路

        Execution (Branch[behaviorTest]);

                //优先执行含有待测行为的支

        Serialization (Branch[]);

    }else if (BehaviorTestCT) {

        Sequential (Trunk);        //顺序执行干路

        Serialization (Branch[]);         //支路串行化

    } else if (BehaviorTestST) {

        Sequential (Trunk);

        Serialization (Branch[]);

    }

End

当有单个待测行为时,详细步骤如下描述:

判断待测行为所在模型的位置, 待测行为位置为干路上时有3种情况:1) 待测行为在前置干路上时;2) 待测行为在中间干路上时;3) 待测行为在后置干路上时。当待测行为在前置干路上时,则对前置干路之后的具有并发行为的支路进行串行化处理,对含有分叉库所的支路不作处理;当待测行为在中间干路上时,需要对回溯寻找中间干路之前含有支路的模块并对模块进行判断,如果具有并发行为,则将并发行为串行化,如果具有分叉行为,则不作处理,对于中间干路之后的支路处理方法则和前置干路之后对支路的处理方法相一致;当待测行为在后置干路上时,回溯寻找后置干路之前的所有含有支路的模块,具有并发行为的将其串行化处理,具有分叉行为的则不作处理。

当待测行为在支路上时,判断支路是并发支路还是分叉支路,如果是并发支路,则先执行含有待测行为的路径,将与待测行为不在同一路径的非待测行为进行串行化的处理,干路不需要作处理;如果是分叉支路,则执行含有待测行为的路径,对于与待测行为不在同一路径的非待测行为加以抑制。

当待测行为在并发变迁上时,如果模型没有出现汇合节点,则将支路上的非待测行为进行串行化的处理;如果出现汇合点,则判断汇合节点类型;当汇合节点为同步变迁时,则将并发变迁后的非待测行为做串行化处理,模型中的干路不作处理;如果汇合节点为同步库所时,则需要将并发变迁后的非待测行为也进行串行化处理,将所有token执行到汇合库所后,再进行下一步操作。

当待测行为在汇合变迁上时,需要回溯寻找含有此汇合变迁的模块的初始节点,当模型中含有并发变迁时,遍历寻找其各支路最长汇合节点,如果最终汇合节点为汇合变迁时,在汇合节点之前的支路需要作串行化处理,当汇合到汇合变迁后,再执行下一动作;当模型中含有分叉库所,且最终汇合到汇合库所时,在单token的情况下,此模型执行不到最终末库所,因此这一情况暂时不作考虑。

算法3    多个待测行为时的算法。

当有多个待测行为时,建立待测行为集,并根据一定的化简顺序进行非待测行为的化简。

Begin

    SetBehaviorTest[];         //对SM中所有变迁遍历寻找

    //待测行为所在模型位置并建立待测行为集

    SIMP (SM);         //递归调用处理模型中的子模块

End

//以下为递归函数SIMP (Modular),用于处理模型SM中的子模

//块嵌套

SIMP (Modular){

    For each i in SetBehaviorTest[]

        If (SetBehaviorTest[i]∈CTSetBehaviorTest[i]∈ST) {

            If (Modular exist SubModular[]) {        //模型中出现模块嵌套

                For each m in SubModular []

                    SIMP (SubModular [m]);

            Simplification (Modular CT‖Modular ST);         //特殊节点

        }

        Simplification (Modular Branch);         //支路

        Simplification (Modular Trunk);         //干路}

当有多个待测行为时,需要对待测行为建立待测行为集:如果集合中待测行为所在位置有特殊节点时,包括CTST,则按特殊节点出现顺序优先化简含有特殊节点的模块;然后再按顺序对支路的与待测行为不再一条路径的非待测行为根据上述规则进行化简,待测行为在干路上时,对化简后的模型再进行判断,如果满足化简规则,则继续化简,否则不再进行化简;当模型中某一模块的支路为下一模块的干路时,化简顺序为先化简最内层模块,再化简外层模块;如果特殊节点为先后顺序时,则化简顺序依次根据特殊节点出现的先后顺序对模块进行化简。综上,化简优先级为RankSpecial node > RankBranch > RankTrunk。当模型中出现分叉库所时,对于起始点为该库所的支路将保留一条与待测行为无关的分支,以便于可以执行模块后边的行为。

3 算法应用

图 4是一个待测软件控制流模型[14], 里边包含了并发、分叉、汇合、嵌套等软件中常见可能性,通过这个模型来说明化简方法的通用性。当有单个待测行为时,本文以t0为例来说明算法应用。

图 4 系统模型[14] Figure 4 System model[14]

示例1    单个待测行为。

第1步    首先对模型进行遍历,记录所有节点对应的输入弧与输出弧,其中:只有输出弧的库所为p0,即p0为初始库所;只有输出弧没有输入弧的库所为p14p12,即此系统模型的末库所不唯一;有单个入弧与多个出弧的节点有1个,为t1;有多个入弧与单个出弧的节点有3个,分别为t4p7p11;有多个入弧与多个出弧的节点有一个,为t7;有单个入弧与单个出弧的节点有21个,分别为t0p1p2p3p4t2t3p5p6t5p13t11、t6p8p9p10p15t8t9t12t10

第2步    判断出模型中的干路与支路,其中干路为图 4中虚线直角矩形所示,分别为p0-t0-p1p7-t6-p8p11-t10-p12;支路为图 4中包含特殊节点的圆角矩形标注所示,分别为p2-t2-p5p3-t3-p6p4-t5-p9-t9p13-t11-p14p9-t8p15-t12p10-t9

第3步    通过第1步模型遍历可以找到系统模型中含有并发变迁t1、同步变迁t4、汇合库所p7、同步并发变迁t7、汇合库所p11;将模型分块,t1并发后,有一条支路并没有到达汇合库所或者汇合变迁,而是到达不同状态,因此,系统模型的末状态不唯一;图 4中的圆角矩形标注即为对系统模型的分块处理。

第4步    深度优先遍历系统模型,寻找待测行为所在位置,由图 4可知,待测行为t0在模型的干路,且在支路之前,因此属于算法总结中的待测行为在干路上的情况,所以需要对不同类型模块进行串行化,如图 5所示。根据规则分别在p2t3之间添加抑制弧,p4t11之间添加抑制弧,p9t12之间添加抑制弧,p9t9之间添加抑制弧,p2t5之间添加抑制弧,p3t5之间添加抑制弧,p4t11之间添加抑制弧,p2t11之间添加抑制弧,p14t9之间添加抑制弧。

图 5 加入优先级的系统模型 Figure 5 System model after adding priority

在没有加入执行优先级之前,原模型状态空间节点个数为532,加入执行优先级之后状态空间节点个数变为167,缩减了365个节点,缩减率为69%。

示例2    多个待测行为。

为了保证算法的通用性,本文仍然选择上述系统模型来对算法进行说明,待测行为集为{t0t4t8}, 模型如图 6所示。

图 6 含待测行为系统模型 Figure 6 System model including tested behavior

第1步    与单个待测行为方法一致,在此不作赘述;

第2步    对于模型支路与干路的判断与上述方法一致;

第3步    遍历寻找模型特殊节点并对模型进行分块方法与单个待测行为时一致;

第4步    深度优先遍历系统模型,寻找待测行为所在位置,建立待测行为集{t0, t4, t8},由图 4可知待测行为t0在模型的前置支路上,t4在模型子模块中的同步变迁点上,t8位于子模块的支路上,因此根据多token执行化简优先级规则,先化简含有特殊节点的含有待测行为的子模块,再化简待测行为在支路上的模块,分别将每一个含有分支情况的子模块中的非待测行为进行串行化处理,方法与单个待测行为算法相同,即根据相关规则在库所与变迁之间添加抑制弧,最终加优先级的模型如图 7所示。

图 7 化简后的系统模型 Figure 7 System model with simplification

原模型状态空间节点个数为532,加入执行优先级之后状态空间节点个数变为284,缩减了248个节点,缩减率为47%。

通过示例1~2发现,本文算法对模型的化简率有一个较大的提升,因此状态空间缩减效果好;其次,对模型化简之后关于模型的测试生成效果是没有改变的。在覆盖待测行为的测试生成方法中,对于与待测行为无关的非待测行为的并行执行采取的办法是只取其中一条执行序列,化简后,由于优先级的作用,使得非待测行为的执行只有一种可能,所以状态空间中仅剩一条序列。所以,化简后生成的序列效果不变,而且效率提升。

4 结语

本文提出了针对待测行为的并行模型化简算法,根据系统模型中待测行为所在模型位置的不同,对非待测行为设定了执行优先级,从而将状态空间节点进行了大幅度的缩减,通过并行模型化简实例验证了本文方法能够大幅缩减并行软件模型的状态空间规模,化简前后对待测行为进行全覆盖测试的测试序列效果不变,从而证明了化简后并没有影响模型的正确性,即本文算法服务于针对待测行为的全覆盖测试序列生成,从根本上提升了并行软件测试序列生成的效率,也为解决复杂的并行软件测试问题奠定了基础[15]

参考文献
[1] 颜炯, 王戟, 陈火旺. 基于模型的软件测试综述[J]. 计算机科学, 2004, 31(2): 184-187. ( YAN J, WANG J, CHEN H W. Survey of model-based software testing[J]. Computer Science, 2004, 31(2): 184-187. )
[2] LEYE S, HIMMELSPACH J, UHRMACHER A M. A discussion on experimental model validation[C]//Proceedings of the UKSim 2009:11th International Conference on Computer Modelling and Simulation. Washington, DC:IEEE Computer Society, 2009:161-167.
[3] SUN T, YE X. A model reduction method for parallel software testing[EB/OL].[2016-06-20]. http://www.emis.ams.org/journals/HOA/JAM/Volume2013/595897.pdf.
[4] 杜秀娟. 基于UML状态图的软件测试用例生成方法研究[D]. 西安: 长安大学, 2008. ( DU X J. Research on software test case generation based on UML state diagram[D]. Xi'an:Chang'an University, 2008. ) http://cdmd.cnki.com.cn/Article/CDMD-11941-2009066192.htm
[5] 孙涛. 基于CP-nets模型的并行软件测试方法研究[D]. 呼和浩特: 内蒙古大学, 2012. ( SUN T. Research on testing method for parallel software based on colored Petri nets[D]. Hohhot:Inner Mongolia University, 2012. ) http://cdmd.cnki.com.cn/Article/CDMD-10126-1013292809.htm
[6] RAI V, SIVASUBRAMANIAN S, BHULAI S, et al. A multiphased approach for modeling and analysis of the BitTorrent protocol[C]//Proceedings of the 27th International Conference on Distributed Computing Systems. Washington, DC:IEEE Computer Society, 2007:10.
[7] 胡乃文. 基于改进蚁群算法的测试序列优化算法[D]. 北京交通大学, 2015. ( HU N W. The algorithm of test sequence optimization based on the improved ant colony algorithm[D]. Beijing:Beijing Jiaotong University, 2015. ) http://cdmd.cnki.com.cn/Article/CDMD-10004-1015558159.htm
[8] 陆公正. 基于EFSM模型的测试用例优化生成及实例化[D]. 上海: 上海大学, 2014. ( LU G Z. EFSM model based optimal generation and instantiation of test cases[D]. Shanghai:Shanghai University, 2014. ) http://cdmd.cnki.com.cn/Article/CDMD-10280-1015574441.htm
[9] SUN T, YE X, LIU J. A test generation method based on model reduction for parallel software[C]//Proceedings of the 201213th International Conference on Parallel and Distributed Computing, Applications and Technologies. Washington, DC:IEEE Computer Society, 2012:777-782.
[10] ZHU H, HE X. A methodology of testing high-level Petri nets[J]. Information and Software Technology, 2002, 44(8): 473-489. doi: 10.1016/S0950-5849(02)00048-4
[11] JENSEN K. An introduction to the theoretical aspect of colored Petri nets[C]//REX1993:Reflections and Perspectives. London:Springer-Verlag, 1994:230-272.
[12] RUSHBY J. Automated Test Generation And Verified Software[M]. Berlin: Springer-Verlag, 2005 : 161 -172.
[13] LEE G, MORRIS J, PARKER K, et al. Using symbolic execution to guide test generation:research articles[J]. Software Testing Verification & Reliability, 2005, 15(1): 41-61.
[14] 李华, 叶新铭. 基于Petri网的控制流与数据流相结合的协议测试[J]. 内蒙古大学学报 (自然科学版), 1999, 29(5): 702-705. ( LI H, YE X M. Protocol test based on the combination of control flow and data flow based on Petri net[J]. Journal of Inner Mongolia University (Natural Science Edition), 1999, 29(5): 702-705. )
[15] SARGENT R G. Verification and validation of simulation models[C]//Proceedings of the 40th Conference on Winter Simulation. Piscataway, NJ:IEEE, 2013:37-48.