基于符号模型检测的Web服务组合形式化验证∗

张世杰 徐 鹏 刘沛瑶

（1.西南交通大学数学学院 成都 610031）

（2.系统可信性自动验证国家地方联合工程实验室 成都 610031）

1 引言

面向服务的体系结构SOA（Service Oriented Architecture）是一种构建分布式系统的方式，将功能作为服务提供，强调交互服务之间的松散耦合［1］。Web服务随着SOA的提出而不断发展，其是SOA体系结构的基本单元，是一种新型的Web应用［2］。随着经济的发展与用户需求的多样化和综合化，单一Web服务所提供的功能已经不能满足需求，因此产生了Web服务组合（Web Service Composition，WSC）。WSC可以集成现有的异构服务而组合成可以提供更复杂功能的新服务，实现更高的服务可重用性和获取增值服务［3］。但WSC也带来了一些新的挑战：如何保证Web服务组合过程的正确性？如何验证组合服务满足某些需要的特性？如何对WSC进行有效的建模、分析和验证？

Web服务组合问题包括：Web服务发现，Web服务组合及组合Web服务的形式化验证。本文研究的重点是组合Web服务的形式化验证，其是保证组合Web服务正式发布投入市场运行，减小其故障的重要手段。常用的服务组合验证方法是69%的模型检查，进程代数的使用率为29%，定理证明方法应用于9%的被调查机制。Web服务组合验证广泛使用的建模工具是NuSMV（22%），SPIN（17%），CPN（12%），UPPAAL（12%），Event-B（10%）和PAT（5%）［4］。

基于Petri网及进程代数的演绎验证方法验证能力很强，但自动化程度不高验证过程需要大量人工参与，当组合Web服务系统比较庞大时就变得相当复杂。沈华等［5］在基于随机Petri网的Web服务组合模型WSCPAM的基础上，提出了对模型进行有界性、死锁、陷阱验证的必要性、意义和算法实现。倪悦等［6］提出一种语义Web服务组合模型到着色Petri网组合模型的转换方法，给出了组合服务的语义一致性验证算法，以一个协同设计过程为例对组合服务流程进行仿真验证并在工作流引擎中部署执行。文献［7］提出某种转换规则将描述Web服务组合的BPEL文件转化为具有直观性的Petri图，通过对Petri图的相关性质找出BPEL的不足之处。文献［8］提出基于扩展有限自动机验证组合Web服务的办法，不但可以验证组合Web服务是否满足系统需求，还可以验证运行过程是否有逻辑错误。胡静等［9］在多元Pi-演算的基础上给出Web服务的描述模型、子类型关系定义和可替换性定义，并对Web服务的相容性进行细化；基于定义给出正确性判定规则和可替换性判定方法。

基于穷尽搜索的模型检测验证方法自动化程度很高、验证速度快、效率高、适用于Web服务数量比较多的组合服务，并且如果一个性质不满足时会给出一个反例，有利于改进组合Web服务。该方法的难点在于如何将现实的服务组合系统转化为对应的数学模型。Babin等［10］提出一种基于Event-B进行细化的新颖的正确构造形式方法，解决了Web服务补偿的功能正确性问题。文献［11］提出了将BPEL定义的服务组合转化为UPPAAL模型进行自动验证的方法。EL KASSMI等［12］使用FSM（有限状态机）对某些安全需求进行建模，使用模型检测工具UPPAAL验证Web服务组合中的形式化和集成方法。周女琪等［13］将Web服务组合过程建立为定量多目标马尔可夫决策过程，并将该模型转化为PRISM模型，同时将不同的用户需求建模为多目标时序逻辑公式，最后使用PRISM验证。

针对Web服务组合形式化验证问题仍存在的不足，如时间复杂度较高、状态爆炸、建模难度较大、验证结果不够精确等，本文提出基于符号模型检测的组合Web服务验证方法。该方法能够缓解状态爆炸问题从而验证比较复杂且服务数量较多的组合Web服务，易于构建形式化模型且可根据反例改进模型。具体工作为将Web服务实例转换为基于消息会话的有限状态自动机模型，通过状态迁移图构建形式化模型并给出时序逻辑表示的性质规约，用符号模型检测器NuSMV自动验证组合Web服务交互的正确性和死锁。

2 模型检测

模型检测是一种通过穷尽搜索所有可能的系统状态自动检测有限状态系统是否满足其设计规范的验证技术，包括两方面：一方面将实际系统建模成模型检测器能够识别的形式化模型；另一方面用线性时序逻辑（Linear Temporal Logic，LTL）、分支时序逻辑（Computation Tree Logic，CTL）等描述系统的性质。模型检测原理如图1所示，输入是模型和性质，输出结果为TRUE时说明性质满足，输出结果为FALSE时说明性质不满足并给出反例。状态空间爆炸是制约模型检测发展的最大问题，减少状态爆炸问题的主要技术有偏序规约、抽象和对称等，而符号模型检测能有效缓解状态爆炸。

图1 模型检测原理图

常用的模型检测工具有SPIN，UPPAAL，NuSMV，PRISM，其中NuSMV（New Symbolic Model Verifier）是Carnegie Mellon University（CMU）的Mc⁃Millan博士在SMV基础上再构造、再实现和扩展的，是第一款基于BDDs（Binary Decision Diagrams）的符号模型检测器［14］。NuSMV形式化模型是由模块化构成的状态迁移系统，通常将实际系统中的每一个实体角色建模为一个模块，但必须有一个主模块，类似c和c++。形式化模型中VAR语句表示变量声明，ASSIGN语句表示变量的赋值和迁移关系，SPEC语句表示系统的属性规约。属性规约可以由时序逻辑公式（LTL和CTL）、不变表达式（invariant expression）以及能够计算从一个指定状态到另一个指定状态的最小或最大路径的表达式表示。

LTL公式由原子命题、时间模态算子和逻辑连接符组成。其中时间模态算子有X（下一个状态），G（所有未来状态），F（某个未来状态），U（直到），R（释放）；逻辑连接符有：┓（否定），∧（合取），∨（析取），→（蕴涵）。LTL公式定义如下：

1）命题常量（true，false）和原子命题变元p是LTL公式；

2）若f，g是LTL公式，则┓f，f ∧g，f ∨g，f →g也是LTL公式；

3）若f，g是LTL公式，则X f，G f，F f，f U g，f R g也是LTL公式；

4）每个LTL公式都可以通过有限次数运用1）、2）、3）得到。

CTL公式由一对操作符表示，第一个操作符是路径量词A（对所有的路径）或E（存在一个路径）；第二个操作符是时态运算符，包括G（global）、F（fi⁃nal）、X（next）和U（untill）。例如，AG（f）表示公式f在所有路径的所有状态都满足，即f总是满足的；EF（f）表示存在一个路径的某个状态使得f满足。

3 Web服务组合的形式化定义

Web服务组合的交互行为可以通过服务之间发送消息和接送消息改变服务内部状态而完成，即从其他服务获取输入消息，经过处理后将消息发送，所以从本质上来讲Web服务是一个状态迁移系统。有限状态自动机作为描述有限状态迁移系统的一种抽象数学模型［15］，与基于一组状态迁移进行表达的Web服务组合优化类似，因此使用有限状态自动机来建模Web服务组合非常合适。基于消息会话的Web组合服务有限状态自动机的形式化定义如下所示。

定义1Web服务有限状态自动机。满足下列条件的一个六元组WM=＜S，s0，F，Mr，Ms，δ＞称为Web服务有限状态自动机，其中：S=＜s0，s1，s2，…，sn＞是非空有限状态集，∀si∈S称为WM的一个状态；s0∈S是初始状态；F ⊆S是终止状态集，∀si∈F称为终止状态；Mr={mr1,mr2,…,mrn}是非空有限接收消息集；MS={mS1,mS2,…,mSn} 是非空有限发送消息集；δ:S×Mr→S或δ:S×MS→S称为状态迁移函数，即(s,mr)∈S×Mr有δ(s,mr)=s′，表示Web服务有限状态自动机WM在状态s接收消息后状态迁移到s′，(s,mS)∈S×MS有δ(s,mS)=s′，表示WM在状态s发送消息后将状态迁移到s′。

定义2多个Web服务交互模型的形式化定义。WM1，WM2，…，WMn是n个Web服务有限状态自动机，它们的交互模型为n个服务的同步积自动机［16］，即

其中：S1||2||…||n=S1×S2×…×Sn是同步自动机的状态集；

4 形式化模型

我们将Web服务的操作用有限状态自动机消息的发送和接收表示，状态用有限状态自动机的状态表示，当执行单一服务中的操作时组合Web服务的状态将会改变。Web服务组合的基本流程有四种结构：顺序组合，并发组合，选择组合和循环组合，其有限状态自动机分别如图2、3、4、5所示。其中Si表示状态，Mr和Ms分别表示接收的消息、发送的消息，WMi表示单一服务的有限状态自动机。

图2 Web服务组合的顺序结构

图3 Web服务组合的并发结构

图4 Web服务组合的选择结构

基于符号模型检测的Web服务组合形式化验证过程是将服务组合系统建模为一个有限状态迁移系统模型，模型中状态间的迁移模拟实际系统的运行，需验证的系统性质用CTL和LTL描述，NuSMV实现形式化模型自动验证。具体建模步骤有三步：

1）为每一个参与交互的Web服务构建有限状态自动机。每个服务用一个有限状态自动机表示，画出其状态迁移图。集合Mr和Ms分别表示此服务与其他服务交互时的接收消息集和发送消息集。服务接收或者发送消息后状态发生迁移，用有向箭头上标记的接收或发送消息表示。

图5 Web服务组合的循环结构

2）构建形式化模型。NuSMV建模语言描述1）中已画出的状态迁移图，CTL和LTL描述需要验证的性质条件。构建模型时采用模块化结构，每一个服务（即自动机）用一个模块表示，并且用关键词process修饰。由于模型中消息集元素众多，所以用一个布尔型数组表示，每一个数组元素对应一个接收消息或者发送消息。

3）验证形式化模型。如果性质不满足将会给出一个反例向用户报告错误的原因，通过验证结果，可以分析服务交互的正确性和死锁状态。

5 实例验证

本文以在线图书订购服务（online bookshop service）为例使用符号模型检测器NuSMV形式化验证组合服务。该组合服务包括4个独立的Web服务，分别是前台服务（windows service）、书店服务（bookshop service）、出版社服务（publisher service）、托运服务（shipper service），交互过程如图6所示。

图6 在线图书订购服务

当前台服务接收到购买者的订单请求后，向书店服务发送一个订单消息order，书店服务收到该消息后，检索出图书的编码号isbn，并通过发送一个查询消息query，通知出版社服务向购买者发送图书；出版社服务收到该消息后会发送一个存货消息inventory，告知书店服务目前该书的库存情况；书店服务收到inventory消息后会向前台服务发送一个账单消息bill，而前台服务在接收到该消息后会通知购买者支付账单并发送一个账单处理消息handbill；出版社服务在接收到该消息后向托运服务发送请求托运消息consign，通知其向购买者运送该图书；而托运服务会返回确认消息notify。

5.1 构建有限状态自动机模型

根据在线图书订购服务的交互描述及定义1构建每个Web服务的有限状态自动机模型，分别用WM1表示前台服务，WM2表示书店服务，WM3表示出版社服务，WM4表示托运服务。以出版社服务为例，其有限状态自动机WM3=＜S,s0,F,Mr,Ms,δ＞，其中：有限状态集S={p0，p1，p2，p3，p4，p5}有6个状态；s0=p0为初始状态；F=p5为终止状态；接收消息集Mr=｛query，handbill，notify｝，发送消息集Ms=｛inventory，consign｝；状态迁移函数δ={{p0,query,p1},{p1,inventory,p2},{p2,handbill,p3},{p3,consign,p4},{p4,notify,p5}}。图7为出版社服务的状态迁移图，P0表示初始状态，带方向的箭头指向初始状态，终止状态P5用环形圈表示，有向箭头表示状态迁移，箭头上标记的消息（？代表接收消息，！代表发送消息）表示状态迁移的条件。同样的方法给出前台服务、书店服务、托运服务的状态迁移图，如图8、图9、图10所示。

图7 出版社服务（publisher service）的状态迁移图

图8 前台服务（windows service）的状态迁移图

图9 书店服务（bookshop service）的状态迁移图

图10 托运服务（shipper service）的状态迁移图

5.2 构建形式化模型

根据状态迁移图构建网上图书订购服务的形式化模型，如图11所示。形式化模型由5个模块构成，包括1个主模块和4个子模块。4个子模块分别对应前台服务、书店服务、出版社服务和托运服务，前面使用process关键词，使得模块异步合成。模型中以“--”开头的为注释语句表示本例中的消息数组，每一个数组元素都是布尔类型且对应一个消息，如message［1］对应订单消息order，数组元素初始值为FALSE，当消息被发送时值变为TRUE。sw表示前台服务的状态集，包括4个状态分别为w0，w1，w2，w3；sb表示书店服务的状态集，包括5个状态分别为b0，b1，b2，b3，b4；sp表示出版社服务的状态集，包括6个状态分别为p0，p1，p2，p3，p4，p5；ss表示托运服务的状态集，包括3个状态分别为s0，s1，s2。状态的迁移通过消息的接收和发送实现，状态值及消息值的变化由ASSIGN语句实现。

图11 部分NuSMV模型

时序逻辑公式LTL和CTL表示系统的性质约束，本例判定服务组合有无死锁状态（失配现象）及服务组合交互过程是否正确。公式如下所示，其中有无死锁状态用LTL公式表示，LTLSPEC语句实现；正确性用CTL公式表示，SPEC语句实现。

1）死锁状态（失配现象）：LTL公式GF（（pr1.sw=w3）&（pr2.sb=b4）&（pr3.sp=p5）&（pr4.ss=s2））表示每一个服务的状态都会到达终止状态，若该公式为TRUE则不存在死锁状态。

图12 死锁及正确性验证实验结果

2）正确性：CTL公式AG（（pr1.sw=w1-＞AX pr2.sb=b0）&（pr2.sb=b1-＞AX pr2.sb=b2）&（pr2.sb=b2-＞ AX pr3.sp=p0）&（pr3.sp=p1-＞ AX pr3.sp=p2）&（pr3.sp=p2-＞AX pr2.sb=b2）&（pr2.sb=b3-＞AX pr2.sb=b4）&（pr2.sb=b4-＞AX pr1.sw=w1）&（pr1.sw=w2-＞AX pr1.sw=w3）&（pr1.sw=w3-＞AX pr3.sp=p2）&（pr3.sp=p3-＞AX pr3.sp=p4）&（pr3.sp=p4-＞AX pr4.ss=s0）&（pr4.ss=s1-＞AX pr4.ss=s2）&（pr4.ss=s2-＞AX pr3.sp=p4）&（pr3.sp=p4-＞AX pr3.sp=p5））刻画了网上图书订购服务的完整交互过程，通过对满足该CTL公式的状态进行标记，可以判断服务组合的正确性。

5.3 验证结果

本文构建的形式化模型的服务组建数量为4个，状态数达到160个，符号模型检测器NuSMV对其进行验证未出现状态爆炸问题，实验结果如图12所示。实验结果表明验证死锁性质的公式为false并给出了反例，即4个服务之间存在死锁状态（失配现象）。由定义2得到4个服务的同步积自动机WM1||WM2||WM3||WM4，并分析实验结果得到反例为（w0，b0，p0，s0），（w1，b0，p0，s0），（w1，b1，p0，s0），（w1，b2，p1，s0），（w1，b2，p2，s0），（w1，b3，p2，s0），（w1，b4，p2，s0）。（w1，b4，p2，s0）为死锁状态，此时WM2已经运行到终止状态，而其余3个服务都没有到达终止状态。

实验结果也表明验证服务组合交互过程正确性的公式为false，即4个Web服务之间的交互是不正确的。分析实验结果给出的反例对服务组合交互过程进行改进，如图13所示在原模型中添加语句：&message［1］，即在前台服务中当初始状态w0迁移到状态w1时使message［1］的值为TRUE。同样在书店服务、出版社服务、托运服务中，初始状态迁移到下一个状态时使对应的消息值为TRUE，而模型其他部分不改变。

图13 改进后的模型

验证改进后的模型得到实验结果如图14所示，实验结果表明CTL公式值为TRUE，说明4个服务之间的交互正确。由实验结果可以得到网上图书订购服务的状态迁移过程，即由4个服务的初始状态的组合（w0，b0，p0，s0）开始，状态迁移过程为（w1，b0，p0，s0），（w1，b1，p0，s0），（w1，b2，p0，s0），（w1，b2，p1，s0），（w1，b2，p2，s0），（w1，b3，p2，s0），（w1，b4，p2，s0），（w2，b4，p2，s0），（w3，b4，p2，s0），（w3，b4，p3，s0），（w3，b4，p4，s0），（w3，b4，p4，s1），（w3，b4，p4，s2），（w3，b4，p5，s2），状态（w3，b4，p5，s2）表示4个服务的终止状态的组合。

图14 正确性验证实验结果

6 结语

本文针对Web服务组合形式化验证问题的不足，提出了基于符号模型检测的Web服务组合形式化验证的方法，给出了基于消息会话的Web服务有限状态自动机的形式化定义和多个Web服务组合的有限状态自动机的形式化定义，详细说明了使用模型检测验证Web服务组合性质的过程。最后通过一个实例对死锁状态和交互正确性验证，并对正确性验证的实验结果给出的反例进行分析，给出改进的形式化模型，得到的实验结果说明了本文方法的可行性。实验结果表明未出现状态爆炸，该方法也适用于其他状态数量较多的Web服务组合验证。下一步将探讨如何高效快速地对更复杂的Web服务组合进行形式化建模，将对其他性质进行验证以及将本文方法与业务流程执行语言BPEL描述的Web服务组合结合。