一种基于NuSMV的服务组合规则路由的正确性验证方法

摘要

本发明公开了一种基于NuSMV的服务组合规则路由的正确性验证方法。本发明首先对于每一个原子服务，建立表示整个业务流程的组合服务模型六元组。其次为组合服务模型服务六元组定义一个NuSMV验证程序的状态变量，根据组合服务模型六元组的消息集合创建NuSMV验证程序的消息变量。然后得到状态变量的所有条件分支及赋值。最后输入待验证的性质，运行生成的NuSMV验证程序，对性质进行验证，对于不满足的性质给出反例。本发明所提供的方法在传统的有限状态机的五元组基础上，扩充了对消息接收和发送的表示，提出了定义企业服务总线上的服务模型六元组，有效地表达了服务和规则的交互情况。

说明书

技术领域

本发明属于Web服务组合规则的形式化验证领域，具体涉及到一种基于模型检测的服务规则路由的正确性验证方法。

背景技术

随着企业信息化的发展，传统的软件架构已经不能满足多个应用集成的需求。面向服务架构（Service Oriented Architecture，SOA）思想的提出在一定程度上解决了这个问题。企业服务总线（Enterprise Service Bus，ESB）作为SOA架构主要的基础设施，已经成功应用在电信、金融等多个领域。当使用ESB集成应用系统时，各个应用将自己的业务功能封装为服务部署在总线上，不同应用之间的交互通过服务的组合和交互完成，具体的传输协议和消息格式的转换则由总线实现。ESB减少了应用集成代价，但消息的路由规则分散在代码中，当业务规则改变时，需要修改源代码以应对由此引起的消息路由规则的改变，从而使得系统的维护成本增加。

将业务规则从业务流程中提取出来，即在传统的ESB中引入规则引擎，使得不同服务之间的消息基于独立的规则进行路由，当规则变更时，直接修改相应的规则配置信息即可，可大大降低系统的维护成本。实现基于规则的消息路由，一个核心问题是如何检测消息路由的正确性，例如：组合服务的实际运行结果是否与用户期望的目标结果相一致，是否出现引起死锁的循环调用，等等。

发明内容

本发明针对现有技术的不足，提供了一种基于NuSMV的服务组合规则路由的正确性验证方法。

本发明方法的具体步骤是： 

步骤(1) 对于每一个原子服务，建立表示其规则路由的六元组模型                                               ，其中表示一个原子服务所有状态的集合，表示原子服务的初始状态，表示原子服务的终结状态集合，表示消息集合，表示消息标识集合，表示当前状态接收消息后达到下一状态，表示发送消息后到下一状态，表示服务所有状态之间的转移关系的集合。

步骤(2) 将通过步骤(1)得到的所有六元组模型合并为表示整个业务流程的组合服务模型六元组。

步骤(3) 为组合服务模型服务六元组定义一个NuSMV验证程序的状态变量，取值范围为组合服务模型六元组的状态集合的所有状态元素，初始值为状态变量的初始赋值。

步骤(4) 根据组合服务模型六元组的消息集合创建NuSMV验证程序的消息变量，初始值设置为具有实际意义的取值范围之外的任意一个值。

步骤(5) 由组合服务模型六元组的状态转移关系集合中的初始状态所在的转移关系得到转移后的状态，由此定义对应该状态变量的NuSMV验证程序的next语句（next语句定义状态变量的转换关系）的一个条件及赋值；从该状态及其所在的转移关系得到状态变量的next语句的下一个条件及赋值；依次交替进行，得到状态变量的所有条件分支及赋值，其中状态变量转换关系的next语句的条件包括状态变量的当前值和消息标识对应的消息变量的取值，最终生成NuSMV验证程序。

步骤(6) 输入使用分支时序逻辑CTL或者线性时序逻辑LTL描述的待验证的性质，运行通过步骤(5)生成的NuSMV验证程序，对性质进行验证，对于不满足的性质给出反例。

本发明中NuSMV是一种经典的模型检测工具，本发明所提供的基于NuSMV的服务组合规则路由的正确性验证方法由一组功能模块组成，它们包括：原子服务六元组模型生成模块、组合服务六元组模型生成模块、NuSMV验证程序生成模块和正确性验证模块。

原子服务六元组模型生成模块根据表示服务信息和路由规则信息的服务模型生成每个原子服务的六元组模型。

组合服务六元组模型生成模块合并每个原子服务的六元组模型，生成表示整个业务流程的组合服务六元组模型。

NuSMV验证程序生成模块根据组合服务六元组模型，生成完整的NuSMV验证程序，包括定义状态变量和消息变量以及它们的初始值，使用 next语句定义状态变量的转换关系。

正确性验证模块输入使用分支时序逻辑CTL或者线性时序逻辑LTL描述的待验证的性质，运行NuSMV验证程序，对性质进行验证，对于不满足的性质给出反例。

目前，国内外学者在Web服务的形式化验证上已经进行了深入研究，证明了模型检测技术验证流程正确性的有效性。与传统的验证服务流程不同的是，本方明所提供的方法适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证，在分析服务状态的变换情况时必须同时考虑服务与规则的交互，并最终基于NuSMV实现。另一方面，为解决企业服务总线中的服务与规则的形式化建模问题，本方明所提供的方法在传统的有限状态机的五元组基础上，扩充了对消息接收和发送的表示，提出了定义企业服务总线上的服务模型六元组，有效地表达了服务和规则的交互情况。

附图说明

图1 Mule与Drools的集成框架示意图；

图2 示例贷款审批服务流程图；

图3 示例贷款审批服务的服务和规则定义图；

图4 示例六元组Wcu状态迁移图；

图5 示例六元组Was状态迁移图；

图6 示例六元组Wap状态迁移图；

图7 示例贷款审批服务流程状态迁移图；

图8 示例贷款审批服务验证结果图。

具体实施方式

基于表示有限状态机的五元组，定义企业服务总线上的服务模型为六元组，，其中：

，表示一个服务（指原子服务，下同）所有状态的集合。在任一确定时刻，一个服务只能对应一个确定的状态。

表示服务的初始状态。每个服务都有一个初始状态，代表服务的入口，由此状态开始接收或者发送消息。

表示终结状态集合，且。每个服务都至少包括一个终止状态，达到此状态后不能再接收或发送消息。

表示消息集合。服务的每个状态可以发送或者接收消息然后到达下一状态，表示这些消息的集合。

表示消息标识集合。消息标识表示状态处理的消息和类型：表示当前状态接收消息后达到下一状态，表示发送消息后到下一状态。

表示服务所有状态之间的转移关系的集合，表示为，满足。即：在任一确定时刻，如果服务当前状态，处理消息类型，则下一时刻，服务将达到状态，。

同时，也可使用服务状态转移图表示服务模型六元组。转移图由圆、同心圆、箭头三种基本形状组成，其中：圆表示初始状态或者中间状态，圆中的字母表示状态名称；同心圆表示结束状态，同心圆中的字母表示结束状态的名称；箭头表示状态的转移，即从一个状态转向下一个状态。箭头上的文字使用字母和符号（或）组合的方式，其中字母为消息的名称，和分别表示由箭头前的状态接收消息或者发送消息后到达箭头后的状态。

本发明所提供的基于NuSMV的服务组合规则路由的正确性验证方法的具体实施方式如下：

1）对于每一个原子服务，建立表示其规则路由的六元组模型

不失一般性，假设在ESB中，每个服务由三部分组成：Inbound（入站）、Component（业务组件）、Outbound（出站）。其中Inbound接收外部或者其他服务发送的消息，是服务的入口；Component组件处理具体业务逻辑；Outbound负责把消息发送到其他服务。在规则路由转换为六元组时，首先需要对每个服务进行建模，分别转换为对应的服务模型六元组。

（1）初始状态定义

入站是每个服务开始执行的地方，对应服务模型六元组的初始状态。该状态可以接受其他服务或者外部应用发送的消息，接收消息后，可以将消息传输到Component组件，也可以使用路由器直接发送消息到其他服务，或者使用规则引擎对消息进行断言后再路由。

（2）中间状态定义

使用六元组对服务进行建模，每个服务只有发送消息到其他服务或者从其他服务接收消息后状态才改变。Component组件只是业务功能的实现，并没有对消息进行路由，也没有发生服务间消息的接收和发送，所以消息经过Component组件并没有改变服务的状态。

如果使用了出站Outbound，并且Outbound配置了链式路由器（chaining-router），那么，状态随着消息达到的出站端点而发生改变，直到链式路由器配置的最后一个出站端点。

如果使用规则进行路由，消息由Inbound接收后进入规则引擎的工作内存进行断言，匹配不同的条件，触发相应的动作。这里，如果触发的动作是直接发送消息到其他服务，则进入终结状态。不同规则中可以使用相同类型的消息，如果规则的条件不同，那么触发消息后服务会进入不同的状态。

（3）终结状态定义

如果服务配置了Outbound，并且Outbound使用通过路由器（pass-through-router），则当前状态发送消息后达到终结状态；如果使用多播路由器（multicasting-router）或者消息分解路由器（message-splitter-router），则将消息发送到多个服务，对应多个终结状态，合并后即为终结状态集 ；如果使用链式路由器（chaining-router），则消息发送给最后一个服务后服务到达终结状态。

如果消息触发的规则的动作中只是发送消息到下一个服务，则服务进入终结状态；如果对消息继续断言，则断言后服务进入终结状态。

服务状态集即为上述初始状态、中间状态、终结状态的集合。

（4）消息集合定义

每个服务与其他服务之间的消息交互，包括发送到其他服务的消息和从其他服务接收的消息，这些消息构成了服务的消息集合 。

（5）消息标识集合定义

服务发送消息msg到其他服务，则消息标识为msg-；如果从其他服务接收消息，则标识为msg+。所有的消息标识构成了服务的消息标识集合。

（6）状态转移关系集合生成

状态转移与消息的发送和接收直接关联。当服务由一个状态接收消息或者发送消息后进入下一状态，即存在一个状态转移关系。所有的状态转移关系构成了服务模型六元组的状态转移关系集合。

2）将所有六元组模型合并为表示整个业务流程的组合服务模型六元组

（1）从接收外部请求的服务（流程开始时的服务）对应的六元组开始，搜索的服务状态转移关系集，如果存在一个转移关系包含终结状态，且标识为-（发送的消息），即，那么接着搜索其他六元组中消息与类型相同但标识为+的转移关系， ，将消息置入的消息集合，状态、和置入的状态集合，转移关系和置入的转移关系集合。这里，表示状态到的转移不经过消息处理。将中的状态集合中初始状态和终结状态之外的其他状态及其对应的消息、转移关系置入到相应的集合中。

（2）去掉对应六元组中的初始状态和包含初始状态的转移关系，将中剩余的状态置入的状态集合，剩余的状态关系置入的状态转移关系集合。将替换成，重复步骤（1）。

（3）如果当前六元组中存在状态，没有到其他状态的转移关系，则创建终结状态、转移关系并置入到的相应集合中。

3）生成NuSMV验证程序

NuSMV工具使用NuSMV程序进行验证，因此只有将业务流程对应的组合服务模型六元组转换为完整的NuSMV程序才能进行验证。

（1）变量的定义

每个模块包括两种变量：状态变量和消息变量。为组合服务模型服务六元组定义一个状态变量，取值范围为六元组的状态集合的所有状态元素；根据六元组的消息集合创建相应的消息变量。

（2）变量的初始化

状态变量的初始值即为状态变量的初始赋值；消息变量初始值可设置为在实际取值范围之外任意一个值。

（3）变量的转换

状态变量的转换关系由NuSMV输入语言的next语句定义。从六元组的状态转移关系集合可以推出每一个状态变量的转移关系：由初始状态所在的转移关系得到转移后的状态，由此定义状态变量的next语句的一个条件及赋值；从该状态及其所在的转移关系可以得到状态变量的next语句的下一个条件及赋值；依次交替进行，得到状态变量的所有条件分支及赋值。状态变量转换关系的next语句的条件包括状态变量的当前值和消息标识对应的消息变量的取值。

消息变量的next语句生成过程如下：遍历六元组的消息集合，对于每一个消息，取出六元组状态转移关系集合中该消息对应的标识为-（即发送的消息）的所有转移关系，得到转移前的状态，将该状态和消息变量的当前值作为next语句的条件，然后对消息变量赋值。

4）验证待验证的性质

输入使用分支时序逻辑CTL或者线性时序逻辑LTL描述的待验证的性质，运行NuSMV验证程序，对性质进行验证，对于不满足的性质给出反例。

以下使用贷款审批服务说明如何使用本发明所提供的方法。其中，ESB选用Mule（http://www.mulesoft.org），规则引擎选用Drools（http://www.jboss.org/drools）。                              

图1是Mule与Drools的集成框架示意图，其中DroolsProxy是Mule中的Drools代理。

图2为一个贷款审批服务的示例流程，表述如下：首先，使用Mule和Drools实现贷款审批业务流程建模，服务之间基于规则进行消息路由；然后，使用本发明所提供的方法将消息路由转换为模型检测工具NuSMV输入程序，即将Mule的流程配置信息（mule-config.xml）和Drools的规则配置信息（rules.xml）转换为smv验证程序；最后，使用NuSMV进行正确性验证。

1） 贷款审批服务定义

图2对应的服务和规则见图3，其中包括3个原子服务和4个规则。CustomerService服务用于接收贷款请求；AssessService服务用于对贷款的风险进行评估，即根据用户的个人信息给出风险是高还是低；ApprovalService服务用于对高风险的贷款或者大额贷款申请进行审批。服务之间通过规则进行连接，根据贷款审批服务语义定义4个规则：规则ApplyLow，贷款金额小于10000时触发；规则ApplyHigh，贷款金额大于等于10000时触发；规则RiskLow，风险评估为低时触发；规则RiskHigh，风险评估为高时触发。

下面叙述实现整个贷款流程的具体配置，包括服务的配置、消息实体类的定义和规则的定义。

（1）服务的配置

在mule-config.xml中定义CustomerService、AssessService、ApprovalService3个Flow对应图3中的3个服务。下面定义了CustomerService流的配置：

<flow name="CustomerService">

<inbound-endpoint

ref="loanReceiver" exchange-pattern="request-response"/>

<component>

<singleton-object class="org.mule.integration.IntegrationComponent" />

</component>

</flow>

这里，入站loanReceiver用于接收外部应用发送的贷款请求。IntegrationComponent类是Mule与Drools集成的实现类，用于发送消息到规则引擎进行断言。

类似地，定义流AssessService，其组件类为AssessServiceComponent。当贷款金额小于10000时，请求被发送到AssessService流的AssessServiceComponent类。AssessServiceComponent类实现对贷款申请进行风险评估的业务功能，评估的结果可能是高风险或者低风险。

类似地，定义流ApprovalService，其组件类为ApprovalServiceComponent。当贷款请求风险评估为高风险或者贷款金额大于等于10000时，请求被发送到ApprovalService流的ApprovalServiceComponent组件类。该类实现对贷款申请进行审批的业务功能，审批的结果可能是贷款请求被接收或者拒绝。

（2）消息实体类的定义

定义消息实体类：LoanMessage类表示用户的贷款申请信息，包含姓名、贷款金额等属性；LoanRisk为贷款风险类，包含姓名、贷款金额、贷款风险等属性；LoanApproval表示贷款审批类，包含姓名、贷款金额等属性。

（3）规则的定义

在rules.drl文件中配置图3中的4个规则。以下定义了规则ApplyLow的配置：

rule "ApplyLow"

when

$loanMessage : LoanMessage( amount < 10000)

then

LoanRisk loanRisk = new LoanRisk(); 

riskMessage.setName(loanMessage.getName());

//发送到AssessService服务，进行个人风险评估。

loanRisk = mule.generateMessage("AssessService", riskMessage, 

null, MessageExchangePattern.ONE_WAY); 

insert(loanRisk);//根据风险级别判断

end

这里，贷款金额由消息类LoanMessage的属性amount表示，当amount<10000时，匹配规则ApplyLow，将LoanRisk类型的消息发送到AssessService流，即对贷款风险进行评估。获取评估结果loanRisk，使用Drools关键字insert对风险类消息loanRisk进行断言。

类似地，定义规则ApplyHigh。当amount>=10000时，匹配规则ApplyHigh，将LoanApproval类型的消息发送到ApprovalService流，即对贷款申请进行审批。

类似地，定义规则RiskLow。当风险为低时，匹配规则RiskLow，风险为低时贷款被批准，这里直接在控制台打印出贷款被批准的字符串。

类似地，定义规则RiskHigh。当风险为高时，匹配规则RiskHigh，将LoanApproval类型的消息发送到ApprovalService流进行审批。

2） 贷款审批服务验证

使用NuSMV进行验证贷款审批服务的消息路由，需要首先进行形式化建模：先将服务模型转换为六元组，再将六元组转换为NuSMV输入语言。

（1）服务模型到六元组的转换实现

CustomerService服务发送贷款请求，对应的服务模型为表示为：，其中：

；

；

；

；

；

。

图4是对应的状态转移图。

AssessService为风险评估服务，对应的服务模型为，其中：

；

；

；

；

；

。

图5为对应的状态转移图。

ApprovalService为审批服务，对应的服务模型为，其中：

；

；

；

；

；

。

图6是对应的状态转移图。

根据服务六元组的合并过程，将服务模型、和合并，得到贷款审批服务整个流程的组合服务模型，其中：

；

；

；

；

；

。

图7为合并后的对应的状态转移图。

（2）六元组到NuSMV的转换实现

为简化起见，使用状态名称分别代替。根据六元组到NuSMV输入语言的转换算法对贷款审批服务流程模型进行转换，转换后的smv程序如下所示：

MODULE main

VAR

amount:1..20;

risk : {initRisk, low, high};

approval : {initApproval,yes,no};

status : {s0,s1,s2,s3,s4,s5,s6,s7};

ASSIGN

init(risk) := initRisk;

init(status) := s0;

init(approval) := initApproval;

next(risk) :=

case

status=s3 : {low, high}; --状态是s3时，风险是低风险或者高风险

1 : risk;

esac;

next(approval) :=

case

status=s4 : yes; --低风险，贷款被批准

status=s6 : {yes, no} ; --高风险或者申请金额较高，可能被批准，可能不被批准

1 : approval;

esac;

next(status) :=

case

status=s0 & amount<10 : s1;

status=s0 & amount>=10 : s2;

status=s1 : s3;

status=s2 : s6;

status=s3 & risk=low : s4;

status=s3 & risk=high : s5;

status=s4 : s7;

status=s5 : s6;

status=s6 : s7;

1 : status;

esac;

这里定义贷款金额amount变量为Integer类型，范围为1~20。当实际贷款金额小于10000元时，使用范围为1~9之内的数字表示；贷款金额大于、等于10000元时，使用10~20之内的数字表示。变量risk表示贷款风险，初始值为initRisk，根据状态的转移可以取值低风险low或高风险high。变量approval表示贷款是否被批准，初始值为initApproval，根据状态的转移可以取值贷款被批准yes或不被批准no。使用LTL和CTL描述待验证的6条性质，NuSMV的验证结果如图8所示。

（1）消息变量性质AF(amount>10 -> EF (approval=yes))使用CTL描述，表示如果贷款申请金额大于10000，最终的贷款申请可能会被批准。这条性质是正确的，满足贷款审批流程的要求。

（2）活性性质G(status=s0 -> F status=s7)和G(status=s0 -> F(approval=yes | approval=no))使用LTL描述，分别表示贷款最终会结束和贷款最终被批准或者不被批准。这两条性质都是正确的，满足贷款审批流程的要求。

（3）消息变量性质G((status=s0 & amount=5) -> F(approval=yes))使用LTL描述，表示如果贷款金额为5000，最终贷款会被批准。这条性质的验证结果为False，满足贷款审批流程的要求。如果验证为True，说明Mule与Drools配置错误，需要修改配置文件。

（4）性质G(status=s0 & !(amount>0 & amount<21) -> F(!status=s7))使用LTL描述，表示如果没有提出贷款请求，则不会收到贷款结果。该性质满足要求，验证结果为True。

（5）性质G( status=s0 & amount<10 & risk=low -> F(approval=yes))使用LTL描述，表示如果贷款金额小于10000，并且评估风险为低，则最终贷款被批准。该性质满足要求，验证结果也为True。