Web服务组合的互模拟验证

Open-bisimulation checking of Web Services combination

为检验Web服务组合的实现与用户需求的一致性,在开互模拟形式化理论和检验工具的基础上,提出了一个自动化检验方法。首先,用π-演算分别对用户需求和商业流程可执行语言(BPEL4WS)程序实现建模,然后对它们进行弱开互模拟检验,当它们不互模拟时,检验工具能自动标识关键的不互模拟的BPEL4WS程序片段。最后通过实例说明这一方法的可行性。

In order to check the congruence between the user＇s demand and implementation of Web Services combination, an auto-checking method was proposed in this paper. It was based on the knowledge of open ,π-bisimulation and checking tools. First, the user＇s demand and BPEIMWS program were modeled by π-ealeulus respectively. Then, weak open- bisimulation was done to them. When they were dissimulating, the checking tool can mark the dissimulation part of BPEIMWS program. In the end, a case study was made to show the feasibility of the method.