论文部分内容阅读
Web服务组合研究领域的一个重要问题是如何形式化描述Web服务组合，验证服务组合的正确性，Web服务组合的形式化模型可以用来检查和验证Web服务组合以保证组合的正确性．文章使用模型检查工具SPIN对目前普遍使用的Web服务组合规范BPEL4WS（Business Process Execution Language for Web Services，Web服务业务流程执行语言）模型进行了验证，给出了BPEL4WS语法到Promela形式化模型的转换方法，最后通过一个实例对BPEL4WS表示的服务组合模型的