图3.17所示的是一个航空订票服务、银行服务与客户代理的交互,主要流程如下:首先客户通过客户代理向订票服务请求订票,订票服务收到订票请求后同时向客户代理和银行服务发送付款请求;银行服务收到付款请求信息同时向订票服务和客户代理发送获取机票和客户信息请求;银行服务收到机票和客户信息后,进行转账;如果转账成功,那么银行服务会返回给订票服务付款成功的确认信息,否则银行服务会返回给订票服务付款失败的信息;订票服务收到付款确认信息后,返回给客户代理订票成功的信息,若订票服务收到付款失败的信息,那么就会返回给客户代理订票失败的信息;整个交互过程结束。其中,Req表示请求订票,ReP表示要求付款信息,GTc表示请求机票信息,GCt表示请求客户信息,Tic表示机票信息,Clt表示客户信息,Pay表示付款成功,NoP表示付款失败,Acc表示订票成功,Fai表示订票失败。
图3.17 订票服务、银行服务与客户代理之间的交互
从图3.17可以看出,订票服务中的通道AC2要同时向其他两个服务发送消息ReP,这时可以考虑将订票服务的状态B扩展为下面图3.18中有序的两个状态B和B′,依次发送消息ReP。银行服务中的状态B和状态C与订票服务中的状态B相同,也是同时向多个服务发送或接收多个服务发送的消息,在图3.18中也将这两个状态进行扩展。在扩展之后,整个服务交互过程就变成了一个完全有序的交互过程,这样就可以用一元Pi演算来描述3个服务及其之间的交互。
图3.18 订票服务、银行服务中的状态扩展
这里,给出状态扩展算法用于将同步发送或接收消息的状态转化为多个有序状态。算法3.1的基本思想是:判断服务中每一个状态下接收或发送的消息数,如果消息数大于1,则根据消息个数增加状态,并给每个扩展状态分配一个消息。
算法3.1 状态扩展算法
输入:初始状态有序消息集InitStateInfo[][],初始的状态个数StateNum。
输出:最终状态有序消息集FinalStateInfo[]。(www.xing528.com)
通过算法3.1就可以将图3.17中的Web服务转变成图3.18中的Web服务。下面根据转化后的交互图就可以手动将3个服务描述为Pi演算中的进程。
图3.18中的订票服务Agent可以表达成如下所示的进程PAgent,该进程通过AC1—AC4和AB1—AB4这8个通道与外界进行通信,其中通道AC1、AB1、AB3和AB4为消息接收通道,AC2、AC3、AC4和AB2为消息发送通道。
客户代理服务Client可以表达成如下所示的进程PClient,该进程通过AC1—AC4、BC1和BC2这6个通道与外界进行通信,其中通道AC2、AC3、AC4和BC1为消息接收通道,AC1和BC2为消息发送通道。
银行服务Bank可以表达成如下所示的进程PBank,该进程通过AC2、AB1—AB4、BC1和BC2这7个通道与外界进行通信,其中通道AC2、AB2和BC2为消息接收通道,AB1、AB3、AB4和BC1为消息发送通道。
因此,订票服务、银行服务和客户代理之间的交互就可以表达成如下所示的组合进程P:
下面,利用这一判定定理来验证上述3个服务的兼容性。对图3.18所示的组合进程推演得到如下结果:
以上两个推演过程分别代表了服务Agent、Blank、Client之间存在的两种交互方式,即两条交互路径。而推演的结果表明,3个服务在任何一次交互中,其组合进程表达式最后均变成空进程,即3个服务进程在通过内部一系列同步通信之后均演变成空进程,说明这3个服务是完全兼容的。
免责声明:以上内容源自网络,版权归原作者所有,如有侵犯您的原创版权请告知,我们将尽快删除相关内容。