从BPMN 模型导出组合服务的代数规约＊

余 波

（1.中南林业科技大学涉外学院，湖南 长沙410042；2.国防科学技术大学计算机学院，湖南 长沙 410073）

1 引言

目前，越来越多的复杂商业应用解决方案采用诸如BPEL（Business Process Execution Language）、WSFL（Web Services Flow Language）、XLang（an XML-based extension of Web Services Description Language）等组合服务编程语言，将多个基本或组合服务组织成能够完成业务过程自组的程序。BPEL已经成为基于Web服务开发可执行业务流程的标准之一[1]。业务流程建模标注BPMN（Business Process Modeling Notation）是一种独立于其它流程建模方法的流程建模标准，提供了一套用户易于理解的图形符号和在BPEL 流程建模及其实现之间平滑过渡的有效机制[2]。

Web服务的质量受到高度关注。与模型检验等方法相比，软件测试是一种发现Web服务缺陷或者错误的简便方法。即使参与组合的Web服务在发布之前均经过测试，仍然需要检查BPEL程序的可执行服务组合逻辑是否正确，以及BPEL服务与其它Web 服务组合时是否存在缺陷。由于Web服务对外仅提供被调用的接口信息，隐藏源代码甚至可执行代码，因此Web服务测试需要采用基于规约的测试方法[3]。

代数规约技术出现于20世纪70年代，定义抽象数据类型时具有独立于实现的特点，并且以公理集刻画抽象数据类型的代数语义。基于代数规约的测试方法独立于软件系统的设计与实现，具有自动生成测试用例、判断测试输出和提供测试驱动等优点，已经成功地应用于测试抽象数据类型、过程、类、组件和Web服务等[4～6]。

应用代数测试方法测试组合Web服务时，首先需要解决Web服务的代数规约生成问题。文献[7]提出以统一风格描述抽象数据类型、过程、类、组件与Web 服务描述语言WSDL（Web Service Definition Language）定义的Web服务的代数规约语言CASOCC-WS（Common Algebraic Specification Language of Component and Class for Web Service），给出了由基本Web服务的WSDL 描述转换成代数规约的方法。

本文通过建立BPMN 结构化表示与正则表达式的映射规则，设计由BPMN 模型导出BPEL 服务的以CASOCC-WS表示的代数规约算法。文章结构组织如下：第2节介绍CASOCC-WS；第3节介绍BPMN 及其转换成基调的映射规则；第4节介绍由正则表达式导出项的算法和书写公理等式的启发式规则；第5节介绍一个案例；第6节介绍相关研究工作；最后总结全文。

2 代数规约语言

描述Web 服务的代数规约语言CASOCCWS[7]以描述抽象数据类型、类和组件的代数规约语言CASOCC[4]为基础，两者在语法和语义上基本相同。主要区别在于：后者将操作分为创建子（Creator）、构造子（Constructor）、转换子（Transformer）和观察子（Observer）四类；前者将操作分为观察子、创建子和构造子，构造子部分可选。CASOCC-WS使用的字符集与Java语言的相同。标识符以字母或下划线开头，连接大小写字母、数字和下划线。保留字包括预定义的基本数据类型、Spec、Import、Operations、Var、Axioms、Constructor、Observer和Transformer等。

一个软件系统的代数规约除了定义数据和操作的基调（Signature）外，另一个重要组成部分是刻画软件系统行为属性的公理集合[8]。CASOCCWS描述Web服务的基本单位是规约单元，以关键字“Spec”开始、“End”结束；“Observable”后附带“F”表示该代数规约不可观察或者“T”表示可观察；“Import”后附带引入的类子或者其它分类；“Operations”部分依次是构造子、转换子和观察子的定义；“Axioms”部分描述公理等式；“Vars”部分描述公理中出现的变量。类子即基本类型的分类。XML Schema定义的数据类型即为预定义类子。

代数规约SP＝〈Σ，E〉，基调SI＝〈S，F〉，s1，…，sn，O 是S 的引入分类，且O 是可观察分类，si≠S，0≤i≤n，f 是S 中的操作，0≤k≤n；如果f：s0×…×sk→S，则称f为创建子；如果f：S×s0×…×sk→S，则称f为转换子：如果f：S×s0×…×sk→O，则称f为观察子。基调定义的分类称为主分类。如果x的类型是主分类，操作f作用于参数x 和y，则可记成x.f（y）。

一个项由Var部分声明的变量、Operations部分声明或被引入分类的操作或常数构成。一个公理等式包含标号、等式和可选条件三个部分。一个等号连接两个项就构成一个公理等式。等式中每个包含操作的项由构造子或者以主分类类型声明的变量开始，连接转换子，最后以观察子结束。条件可以是布尔型的项、等式以及逻辑关系式。

代数测试方法的基本思想是，以常数替代公理等式的项的变量，使得该项成为基础项。一条公理包含两个相等的基础项，包含操作的项又能看成是操作所构成的调用序列[5]。因此，测试用例可看作是一个三元组〈T1，T2，Cond〉，T1 和T2 是基础项，Cond 表示具有Boolean类型的条件，该条件可选。当Cond 为空或者其真值为真时，T1和T2的值应该相等。如果不等，则认为该公理所包含的操作中至少存在一个错误。

若Ai是代数规约的一条公理，记LSet＝｛f：s0×…×sk→S｜f在Ai的等号左边的项中出现｝，RSet＝｛f：s0×…×sk→S｜f在Ai的等号右边的项中出现｝，若LSet∩RSet＝Ø，则称Ai是第一类公理。若RSet退化为变量和常量的基本运算表达式，则Ai是包含泛不动点的公理[6]。如果f ∈LSet∩RSet，且f 中包含错误，则该公理可能检测不出。

3 业务流程建模符号

BPMN 图形元素分为流对象、连接对象、泳道和物件四类。流对象定义业务流程；连接对象用于描述流对象间的连接以及建立流对象与物件的关联；泳道用于对基本建模元素分组；物件描述流程的额外信息。BPMN 规范还规定到BPEL 程序的映射。已有多个工具提供BPMN 建模环境。通常以XML来表示应用BPMN 元素建立的组合服务模型。

一个BPEL程序的BPMN 模型是一个有向图G＝〈N，E，Start，Exit〉，节点集合N 中的每个元素是一个BPMN 中的业务流程；边集E 中的每个元素e＝〈n1，n2〉表示从节点n1到节点n2有一条有向边，边即连接对象表示的业务流程间的关系；Start和Exit分别表示子程序的入口和出口节点，Start，Exit∈N。

3.1 转换规则

BPMN 表示转换成基调的规则定义如下：

（1）BPMN 的名称对应代数规约的名称。

（2）对于BPMN 包含的每个消息或者类型定义，如果未曾定义其代数规约，则按文献[7]的类型或者消息转换成代数规约的规则转换之，生成的代数规约的分类名即为该类型的类型名或者消息名；将生成的代数规约的分类名添加至基调的Import列表中。

（3）BPMN中的每个操作和数据类型可映射为基调中的操作的对应定义，即BPMN 定义的每个操作对应基调的一个操作定义；如果返回类型是可观察类型，则将该操作添加至基调的Observer部分；否则添加至Transformer部分；操作的每个输入参数类型，如果没有在Import列表中出现过，则添加至Import列表；对于每个返回类型，如果没有在Import列表中出现过，则添加至Import列表。

3.2 从BPMN 结构到基调的映射规则

假定BPMN 图中节点N 采用五元组〈no，op，ic，oc，nl〉表示，其中，no 表示节点编号，op 表示操作语句，ic表示节点的入度，oc表示节点的出度，nl是链接后继节点的指针。节点表示流程中的任务、嵌入式流程、启动事件、中间事件、结束事件和网关。图1～图6所用运算符号的含义如下：

（1）a；b：表示顺序执行操作a和操作b；

（2）a＊：表示循环执行操作a零次或者多次；

（3）！con＿1：表示对条件con＿1取非；

（4）a｜b：表示并行执行操作a和操作b；

（5）a[]b：表示选择地执行操作a和操作b之一；

（6）（a；b）：表示顺序执行操作a和操作b。

其中，a、b等符号表示操作名，“｛｝”包含的表达式con＿1、con＿2等表示条件。由“；”、“＊”、“！”、“｜”、“[]”、“（）”等运算构成的正则表达式表示一个复合节点。图1～图6分别给出上述六个运算对应到正则表达式的转换规则。

3.2.1 顺序合并规则

如果节点a的出度及其直接后继节点b和c的入度均等于1，则该结构可合并为新节点d，d.no＝a.no＿b.no＿c.no，d.op＝a.op；b.op；c.op，d.ic＝a.ic，d.oc＝c.oc，d.nl＝c.nl。如图1所示。

Figure 1 Rule for sequence图1 顺序流合并规则

3.2.2 条件流合并规则

如果节点a具有两个不同取值，b和d 分别对应a 的不同取值可执行的活动或者消息，而且d 还表示条件归并节点，则该结构可合并为新节点f，f.no＝a.no＿b.no＿c.no＿d.no；f.op＝（a；d）[]（a；b；c；d），f.ic＝a.ic，f.oc＝d.oc，f.nl＝d.nl。如图2所示。

Figure 2 Rule for choice图2 条件结构合并规则

3.2.3 异或网关合并规则

如果节点a表示具有多个数据或者事件取值的网关，b、c、d 分别对应a 的不同取值的活动或消息，e表示异或归并节点，则该结构可合并为一个新节点f，f.no＝a.no＿b.no＿c.no＿d.no＿e.no；f.op＝a；（｛c1｝b[]｛c2｝c[]｛c3｝d）；e，f.ic＝a.ic，f.oc＝e.oc，f.nl＝e.nl。如图3所示。

Figure 3 Rule for XOR图3 异或网关合并规则

3.2.4 循环结构合成规则（循环体至少执行一次）

节点a表示具有多个数据或者事件取值的网关，b、c 分别表示可循环执行的顺序节点，节点d表示具有多个数据或者事件取值的网关节点，则该结构可以合并为一个新节点e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；b；c；（d；a；b；c）＊[]！d.e.ic＝a.ic，e.oc＝d.oc，e.nl＝d.nl。如图4所示。

Figure 4 Rule for loop（loop body executed more than once）图4 循环结构合并规则（循环体至少执行一次）

3.2.5 循环结构合成规则

节点a表示具有多个数据或者事件取值的网关，b、c分别表示循环体内的顺序节点，d 表示网关的另外一个分支节点，则该结构可以合并为一个新节点e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；（b；c）＊[]！a；d；e.ic＝a.ic，e.oc＝d.oc，e.nl＝d.nl。如图5所示。

3.2.6 与网关合并规则

节点a表示具有多个数据或者事件取值的网关，b、c分别对应两个并行的节点，d 表示与归并节点，则该结构可以合并为一个新节点e，e.no＝a.no＿b.no＿c.no＿d.no；e.op＝a；（b｜c）；d，e.ic＝a.ic，e.oc＝e.oc，e.nl＝d.nl。如图6所示。

Figure 5 Rule for loop（Loop body may not execute）图5 循环结构合成规则（循环体可以一次不执行）

Figure 6 Rule for AND gate图6 与网关合并规则

一个BPMN 模型可以看作是一个图G，因此由图G 导出正则表达式的算法如下所述。

算法1 由图导出操作表达式算法

步骤1 遍历BPMN 文档，以操作名和条件名为节点构建图G。

步骤2 深度优先遍历图G，依次识别单入口单出口节点，根据规则3.2.1合并图G。

步骤3 深度优先遍历图G，根据节点间关系，对于单入口多出口结点，按规则3.2.2、3.2.3、3.2.6合并图G；对于多入口单出口结点，按规则3.2.4和3.2.5合并图G。

步骤4 深度遍历图G，如果图G 已经合并成一个复合节点，则结束算法；否则，依次执行步骤2～步骤4。

显然，执行上述算法，图G 最终会合并成一个仅仅包含“（）”、“｜”、“＊”、“！”、“[]”、“；”、操作名和条件名的正则表达式节点。

如果一个BPMN 程序仅仅包含顺序、循环、选择和并行等四种结构，则算法1的执行时间是有限的。假设BPMN 模型的操作节点数为n，条件节点数为m，且m＜n，则算法1 的时间复杂度是O（n2）。

3.3 由正则表达式导出公理

从包含“（）”、“｜”、“＊”、“！”、“[]”、“；”等连接符的正则表达式导出操作调用序列，主要步骤即先先将循环和并行运算转化成由“[]”表示的正则表达式，然后应用算法2从每个“[]”运算正则表达式中抽取一个选择项以构成操作序列。

3.3.1 循环运算

对于一个包含“＊”运算的正则表示a＊，其中a为操作，如果a至少出现一次，则a＊可以表示成a[]（a；a）[]（a；a；a）[]，否则可以将其表示成（）[]a[]（a；a）[]…，其中，“（）”表示空操作。如果操作a的循环次数为k，则选择运算表示的正则表达式的最后一个项即为操作a执行k 次。

3.3.2 并行运算

对于一个包含“｜”运算的正则表示a｜b，a、b均为操作，则可表示成a；b[]b；a。

3.3.3 选择运算

只包含一个选择运算符“[]”的正则操作表达式a[]b，表示分别选择a 或者b 操作；如果包含多个“[]”运算符号，在生成操作调用序列时，由“[]”连接的每个操作均可以被选择一次。

3.3.4 生成操作调用序列

对于由算法1 所导出的正则表达式，按照3.2.1和3.2.2节的规则将循环和并行操作转换成由“[]”连接的表达式，算法描述略。

下面介绍由“[]”和操作构成的正则表达式生成操作调用序列的算法。节点数据结构和指向该操作或者条件的后续节点中的第一个节点、指向同一层级的“[]”连接的兄弟节点和指向该节点有前驱节点的指针，另外一个用于记录节点被遍历次数的域count，一个仅仅包含“[]”运算的正则表达式由链表数组表示。

算法2 仅包含选择操作的表达式生成操作调用序列

根据前面有关操作节点与条件节点个数的假设，算法2的时间复杂度为O（nm）。

3.4 由项导出公理的启发式规则

每个序列可以看作是等式的一个项。对于每个由算法2导出的项，按下面的规则处理。

（1）从根出发，执行算法1，构造从根至终端节点形如｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝的序列seq。

（2）对于每个序列seq，从其包含的谓词处分开，构造如下形式的公理：“｛p1｝t1…｛pi｝＝true，if p1＆＆…＆＆pi；”…；“｛p1｝t1…｛pi｝ti｛pi＋1｝＝true，if p1＆＆…＆＆pi＋1；”…“｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝，if p1＆＆ …＆＆pn＋1；”。

（3）如果一个形如｛p1｝t1…｛pi｝ti｛pi＋1｝ti＋1…｛pn｝tn｛pn＋1｝的序列seq 包含一个观察子ti，则可构造如下形式的公理：｛p1｝t1…｛pi｝ti＝aValue；aValue是人工分析该序列得到的一个表达式或者值，“｛p1｝t1…｛pi｝”是ti的可观察上下文。

（4）如果所定义的基调中的每个改变待测试软件实体的状态操作对应一个将所改变状态还原到该操作执行前的状态的还原操作，则需要在这些操作执行后，逆序添加还原操作，将Web服务的状态恢复到执行测试之前的状态。

（5）如果所定义的基调的改变状态的操作没有对应的还原操作，则包含该操作的序列写在公理等式等号的右边，而等式等号的左边书写不改变状态的序列、表达式或者常值。

上述规则（4）和规则（5）可以避免在执行一次包含两个序列的测试时，前一次测试序列执行对后面的测试序列的执行结果产生副作用。

4 原型工具与案例研究

根据上述算法和规则生成的操作调用序列，可以用于构造公理等式等号左边的项，等号右边的项须由人工完成。从BPMN 模型导出基调的原型工具以BPMN 建模文件（XML文件）为输入，生成由CASOCC-WS描述的组合服务的代数规约框架，而公理等式则需要由测试员补充完整。

Jboss公司发布的组合服务引擎Jbpel附带一个组合服务ATM 示例[9]，其部署环境：Windows XP＋JDK1.5＋Jboss4.2.0 ＋JBPM1.1。ATM服务的BPMN 模型如图7所示。根据以上规则，可得到如下形式代数规约，其中公理由人工完成。

该代数规约仅给出ATM 的部分操作的定义和部分公理，公理表示中“｛…｝”包含前置或后置条件。FrontEnd、Account和TicketIssuer的代数规约在此省略。在公理5中，执行操作F.withdraw（y，d）会改变Web服务的状态，在该公理的等号右边的项的后置条件部分添加操作F.deposit（y，d），以还原操作F.withdraw（y，d）对Web服务的状态变化。

5 相关工作

BPEL 程序测试分为单元测试和集成测试[10]。BPEL 组合服务的测试需要解决如下问题：（1）自动生成测试数据或者测试用例；（2）一个自动运行测试的驱动程序；（3）测试结果判定问题等。已有BPEL测试的工作主要有如下几类：（1）基于模型验证器的测试方法，如测试BPEL服务的一致性[8]；（2）基于BPEL程序结构测试方法，如应用数据流测试BPEL 程序[11，12]，基于图的遍历测试BPEL 程序[13]；（3）基于已有测试框架测试BPEL程序[14]；（4）基于形式化规约测试BPEL 程序[15]等。这些工作主要解决测试数据生成或者测试驱动，对于测试输出的自动判断还是没有提供适当的解决方案[16]。

Figure 7 BPMN model of ATM图7 ATM 的BPMN 模型表示

6 结束语

为了解决应用代数规约测试BPEL 组合服务的代数规约生成问题，本文提出了从BPMN 模型导出BPEL服务的用代数规约语言CASOCC-WS表示的代数规约的方法。该方法可从BPMN 模型中自动导出基调，提出的书写代数规约的启发式规则，可方便测试员书写代数规约。将来的工作包括：进一步改进提出的方法，实现基于代数规约自动测试BPEL服务的工具。

[1]IBM.Business process execution language for Web services version 1.1[EB／OL].[2010-06-28].http：／／www.ibm.com／developerworks／library／specification／ws-bpel／.

[2]OMG.Documents associated with business process model and notation（BPMN）1.2[EB／OL].[2010-07-13].http：／／www.omg.org／spec／BPMN／1.2／PDF／.

[3]Jokhio M S，Dobbie G，Sun J.Towards specification based testing for semantic Web services[C]∥Proc of 2009Australian Software Engineering Conference，2009：54-63.

[4]Kong Liang，Zhu Hong，Zhou Bin.Automated testing EJB components based on algebraic specifications[C]∥Proc of COMPSAC'07，2.07：717-722.

[5]Yu Bo，Kong Liang，Zhang Yu-feng，Zhu Hong.Testing java components based on algebraic specifications[C]∥Proc of ICST'08，2.08：190-199.

[6]Yu Bo，Kong Liang，Peng Chen.Web service test based on algebraic specification[J].Computer Engineering，2009，35（21）：60-61.（in Chinese）

[7]Zhu H，Yu Bo.Algebraic specification of Web service[C]∥Proc of the 10th International Conference on Quality Software，2010：457-464.

[8]Dong Rong-sheng，Wei Zhao，Luo Xiang-yu，et al.Testing conformance of BPEL business process based on model checking[J].Journal of Software，2010，5（9）：1030-1037.

[9]Jboss.WS-BPEL runtime user guide[EB／OL].[2007-11-29].http：／／docs.jboss.com／jbpm／bpel／v1.1／userguide／tutorial.atm.html.

[10]Mayer P.Towards a BPEL unit testing framework[C]∥Proc of International Symposium on Software Testing and Analysis，2006：33-42.

[11]Liu Chien-hung，Chen Shu-ling.Data flow analysis and testing for web service compositions based on WS-BPEL[C]∥Proc of SEKE'09，2.09：306-311.

[12]Mei Li-jun，Chan W K，Tse T H，et al.An empirical study of the use of frankl-weyuker data flow testing criteria to test bpel web services[C]∥Proc of International Computer Software and Applications Conference，2009：81-88.

[13]Yuan Yuan，Li Zhong-jie，Sun Wei.A graph-search based approach to BPEL4WS test generation[C]∥Proc of International Conference on Software Engineering Advances，2006：14-14.

[14]Li Z J，Tan H F，Liu H H，et al.Business-process-driven gray-box SOA testing[J].IBM Systems Journal，2008，47（3）：457-472.

[15]Ma Chun-yan，Wu Jun-sheng，Zhang Tao，et al.Testing BPEL with stream X-machine[C]∥Proc of International Symposium on Information Science and Engineering，2008：578-582.

[16]Ladan，Mohamad I.Web services testing approaches：A survey and a classification[J].Communications in Computer and Information Science，2010，88（2）：70-79.

附中文参考文献：

[6]余波，孔良，彭琛.基于代数规约测试Web服务的工具的设计与实现[J].计算机工程，2009，35（21）：60-61.