一种基于NuSMV模型检测的服务组合编制方法

给出了基于模型检测服务组合方法,该方法形式化定义Web服务以及服务组合模型,使用计算树逻辑描述服务组合模型交互的控制流程,使用符号模型检测工具NuSMV自动检测服务组合模型的总体目标与服务交互的正确性。并通过一个具体案例验证了该服务组合编制方法的正确性和可行性,成功生成一个服务编制器。该方法可以有效缓解服务组合过程中状态爆炸问题,从而降低企业的开发成本及风险。

An Approach to Services Orchestration Based on NuSMV Model Checking

It has been an important research field to ensure the correctness of the service components interaction in service composition research. This paper proposes a service orchestration approach based on model checking, which uses Compute Tree Logic（CTL） to describe the control procedure of the interaction for the service composition model and adopts symbol model inspection tool, named NuSMV, to automatically validate the correctness between the integral target and service interaction. Furthermore, we verify the correctness of our proposed service composition orchestrator method through a concrete application case and successfully generate an orchestrator. Meanwhile, our approach effectively mitigates the state explo- sion problem of service composition, thus reducing the development cost and risk in the enterprise.