在将服务表达成Pi演算进程且将服务之间的交互表达成并行组合进程表达式之后，服务之间兼容性的验证就可以转化为对进程表达式的推演。邓水光[2]给出了在Pi演算中两个服务是否兼容的判定定理，并给出了如下证明过程。
判定定理 给定两个服务s1和s2以及两个服务对应的进程表达式P和Q，若这两个服务是可兼容的，则这两个服务的进程必定满足条件：P|Q⇒0。
证明：①根据服务可兼容的定义可知，若服务s1和s2是可兼容的，则两个服务在交互的过程中，至少存在一条交互路径，使得两个服务均能从服务的起始状态演变成结束状态。此时，进程P和Q可按照该交互路径产生的交互消息链进行内部通信，最终使得P|Q演变成空进程，即条件P|Q⇒0满足。②若条件P|Q⇒0满足，则说明进程表达式P|Q可通过内部同步操作（即进程P和Q之间进行同步通信）演变成空进程，而在演变过程中，P和Q之间形成了一条消息序列s。此时，服务s1和s2根据该消息序列也能使得两个服务均从起始状态到达结束状态，因此服务s1和s2是可兼容的，证毕。
根据上面的判定定理，下面来验证服务间的兼容性。
对式3.6所示的并行进程推演得到如下结果：
以上两个推演过程分别代表了服务A与B之间存在的两种交互方式，即两条交互路径。而推演的结果表明，两个服务在任何一次交互中，其组合进程表达式最后均变成空进程，即两个服务进程在通过内部一系列同步通信之后均演变成空进程。这也印证了这两个推演过程所对应的两条交互路径全部为有效交互路径，因而也说明了这两个服务是完全兼容的。
对式3.9所示的并行进程推演得到如下结果：
以上两个推演过程同样分别代表了服务Ag与C之间存在的两种交互方式，即两条交互路径。而推演的结果表明，两个服务在任何一次交互中，其组合进程表达式最后均变成空进程，即两个服务进程在通过内部一系列同步通信之后均演变成空进程。这也印证了这两个推演过程所对应的两条交互路径全部为有效交互路径，因而也说明了这两个服务是完全兼容的。
这里我们还需要进一步说明，在服务Ag中还包含了服务A和服务B。因此，服务Ag和服务C的兼容性是与服务A和服务B紧密相关的。下面，我们将服务Ag和服务C的交互过程展开，以此来验证3个服务之间的兼容性。
以上两个推演过程分别代表了服务Ag与C之间在限定A和B后存在的两种交互方式，即两条交互路径。而推演的结果表明，3个服务在任何一次交互中，其组合进程表达式最后均变成空进程，即3个服务进程在通过内部一系列同步通信之后均演变成空进程。这也印证了这两个推演过程所对应的两条交互路径全部为有效交互路径，因而也说明了这3个服务是完全兼容的。
再考察图3.10和图3.11所示的交互过程，其中图3.10中A2-B′服务对应的进程表达式为式3.16。
对式3.16所示的并行进程推演得到如下结果：
图3.11中A2服务对应的进程表达式为式3.19。
对式3.16所示的并行进程推演得到如下结果：(www.xing528.com)
以上4个推演过程也分别代表了两个服务之间的一次可能的交互过程，即交互路径；式3.17和式3.21均能使得进程最终演变成空进程，然而式3.18在D2向A2-B′发出消息NTc之后，由于A2-B′无法接收该消息，致使组合进程表达式无法再往下迁移，这说明两个服务在这种情况下无法完成正常的交互，即这个推演过程所代表的交互路径为非有效交互路径，因此服务D2和A2-B′是局部兼容的。同理，式3.20当C2接收消息Ref时，由于A2无法发送该消息，致使组合进程表达式无法再往下迁移，这说明两个服务在这种情况下无法完成正常的交互，即这个推演过程所代表的交互路径为非有效交互路径，因此服务C2和A2是局部兼容的。推演的结果表明，3个服务是局部兼容的。
至此，我们通过手动推演完成了订票服务、客户代理以及机票预订服务这3个服务之间兼容性的验证过程，即进程表达式的推演过程。但在实际应用中，服务间的交互过程要更加复杂，很难手动完成，因此需要借助辅助工具来完成。
本章采用基于New Jersey SML语言编译器的MWB（Mobility Workbench）工具。MWB工具是用于操作和分析移动并发系统的自动化Pi演算工具，它使用函数式编程语言SML构建，具体使用的是朗讯贝尔实验室实现的SML/NJ110版。验证时的软件实验环境为Windows XP、SML/NJ110.0.7版、MWB′99版。
使用MWB工具对代数表达式进行语法分析可以发现进程定义的一些基本错误，如类型错误、缺少同步、不完整的行为等，并可以利用工具的推理功能排除一些最常见的错误。使用deadlocks命令可以检查进程是否存在死锁的情况，而使用step命令可以查看进程行为，即进行系统行为的跟踪推演。
图3.12至图3.15就是使用step命令查看订票服务、客户代理和机票数据服务3个服务间的交互行为是否可从起始状态到达结束状态，如果可以到达结束状态则说明3个服务是兼容的。
图3.12是式3.10在MWB中的推演过程，图中′get表示输出名字get，命令agent P（get，tic，ntc）=′get.（tic.0+ntc.0）表示定义进程P，进程P中包含名字get、tic和ntc，命令step R（get，tic）表示对进程R先后发送或接收消息get和tic的行为跟踪推演。执行完该命令后，输入0表示选取上面3种状态中的第一种状态接着执行，最后执行完，状态达到0，说明两服务兼容。
图3.13是式3.11在MWB中的推演过程，命令step R（get，ntc）表示对进程R先后发送或接收消息get和ntc的行为跟踪推演。执行完该命令后，输入0表示选取上面3种状态中的第一种状态接着执行，最后执行完，状态达到0，说明两服务兼容。
图3.14是式3.12在MWB中的推演过程，命令step R（req，ref）表示对进程R先后发送或接收消息req和ref的行为跟踪推演。执行完该命令后，输入0表示选取上面3种状态中的第一种状态接着执行，最后执行完，状态达到0，说明两服务兼容。
图3.15是式3.13在MWB中的推演过程，命令step R（req，acc）表示对进程R先后发送或接收消息req和acc的行为跟踪推演。执行完该命令后，输入0表示选取上面3种状态中的第一种状态接着执行，最后执行完，状态达到0，说明两服务兼容。
图3.12 step命令1
图3.13 step命令2
图3.14 step命令3
图3.15 step命令4
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
